HEADER.html -- ACL2 Version 2.7

HEADER

return the header of a 1- or 2-dimensional array
Major Section:  ARRAYS

Example Form:
(header 'delta1 a)

General Form: (header name alist)

where name is arbitrary and alist is a 1- or 2-dimensional array. This function returns the header of the array alist. The function operates in virtually constant time if alist is the semantic value of name. See arrays.


[ICO]NameLast modifiedSizeDescription

[DIR]Parent Directory  -  
[TXT]+.html13-Nov-2002 15:43 618  
[TXT]1+.html13-Nov-2002 15:43 513  
[TXT]1-.html13-Nov-2002 15:43 520  
[TXT]=.html13-Nov-2002 15:43 891  
[TXT]ABORT_bang_.html13-Nov-2002 15:43 787  
[TXT]ABS.html13-Nov-2002 15:43 956  
[TXT]ACCUMULATED-PERSISTENCE.html13-Nov-2002 15:43 7.0K 
[TXT]ACKNOWLEDGMENTS.html13-Nov-2002 15:43 5.6K 
[TXT]ACL2-COUNT.html13-Nov-2002 15:43 1.2K 
[TXT]ACL2-CUSTOMIZATION.html13-Nov-2002 15:43 4.7K 
[TXT]ACL2-DEFAULTS-TABLE.html13-Nov-2002 15:43 13K 
[TXT]ACL2-NUMBERP.html13-Nov-2002 15:43 482  
[TXT]ACL2-PC_colon__colon_=.html13-Nov-2002 15:43 4.9K 
[TXT]ACL2-PC_colon__colon_ACL2-WRAP.html13-Nov-2002 15:43 712  
[TXT]ACL2-PC_colon__colon_ADD-ABBREVIATION.html13-Nov-2002 15:43 2.6K 
[TXT]ACL2-PC_colon__colon_BASH.html13-Nov-2002 15:43 1.1K 
[TXT]ACL2-PC_colon__colon_BDD.html13-Nov-2002 15:43 1.0K 
[TXT]ACL2-PC_colon__colon_BK.html13-Nov-2002 15:43 1.1K 
[TXT]ACL2-PC_colon__colon_BOOKMARK.html13-Nov-2002 15:43 972  
[TXT]ACL2-PC_colon__colon_CASESPLIT.html13-Nov-2002 15:43 2.9K 
[TXT]ACL2-PC_colon__colon_CG.html13-Nov-2002 15:43 712  
[TXT]ACL2-PC_colon__colon_CHANGE-GOAL.html13-Nov-2002 15:43 1.1K 
[TXT]ACL2-PC_colon__colon_CLAIM.html13-Nov-2002 15:43 2.4K 
[TXT]ACL2-PC_colon__colon_COMM.html13-Nov-2002 15:43 2.7K 
[TXT]ACL2-PC_colon__colon_COMMANDS.html13-Nov-2002 15:43 1.3K 
[TXT]ACL2-PC_colon__colon_COMMENT.html13-Nov-2002 15:43 728  
[TXT]ACL2-PC_colon__colon_CONTRADICT.html13-Nov-2002 15:43 483  
[TXT]ACL2-PC_colon__colon_CONTRAPOSE.html13-Nov-2002 15:43 1.2K 
[TXT]ACL2-PC_colon__colon_DEMOTE.html13-Nov-2002 15:43 1.5K 
[TXT]ACL2-PC_colon__colon_DIVE.html13-Nov-2002 15:43 1.9K 
[TXT]ACL2-PC_colon__colon_DO-ALL-NO-PROMPT.html13-Nov-2002 15:43 876  
[TXT]ACL2-PC_colon__colon_DO-ALL.html13-Nov-2002 15:43 1.3K 
[TXT]ACL2-PC_colon__colon_DO-STRICT.html13-Nov-2002 15:43 850  
[TXT]ACL2-PC_colon__colon_DROP.html13-Nov-2002 15:43 1.0K 
[TXT]ACL2-PC_colon__colon_DV.html13-Nov-2002 15:43 2.0K 
[TXT]ACL2-PC_colon__colon_ELIM.html13-Nov-2002 15:43 758  
[TXT]ACL2-PC_colon__colon_EQUIV.html13-Nov-2002 15:43 2.7K 
[TXT]ACL2-PC_colon__colon_EX.html13-Nov-2002 15:43 657  
[TXT]ACL2-PC_colon__colon_EXIT.html13-Nov-2002 15:43 3.5K 
[TXT]ACL2-PC_colon__colon_EXPAND.html13-Nov-2002 15:43 1.5K 
[TXT]ACL2-PC_colon__colon_FAIL.html13-Nov-2002 15:43 937  
[TXT]ACL2-PC_colon__colon_FORWARDCHAIN.html13-Nov-2002 15:43 1.4K 
[TXT]ACL2-PC_colon__colon_FREE.html13-Nov-2002 15:43 643  
[TXT]ACL2-PC_colon__colon_GENERALIZE.html13-Nov-2002 15:43 2.2K 
[TXT]ACL2-PC_colon__colon_GOALS.html13-Nov-2002 15:43 723  
[TXT]ACL2-PC_colon__colon_HELP-LONG.html13-Nov-2002 15:43 617  
[TXT]ACL2-PC_colon__colon_HELP.html13-Nov-2002 15:43 2.4K 
[TXT]ACL2-PC_colon__colon_HELP_bang_.html13-Nov-2002 15:43 651  
[TXT]ACL2-PC_colon__colon_HYPS.html13-Nov-2002 15:43 2.7K 
[TXT]ACL2-PC_colon__colon_ILLEGAL.html13-Nov-2002 15:43 811  
[TXT]ACL2-PC_colon__colon_IN-THEORY.html13-Nov-2002 15:43 1.9K 
[TXT]ACL2-PC_colon__colon_INDUCT.html13-Nov-2002 15:43 1.3K 
[TXT]ACL2-PC_colon__colon_LISP.html13-Nov-2002 15:43 2.2K 
[TXT]ACL2-PC_colon__colon_MORE.html13-Nov-2002 15:43 588  
[TXT]ACL2-PC_colon__colon_MORE_bang_.html13-Nov-2002 15:43 651  
[TXT]ACL2-PC_colon__colon_NEGATE.html13-Nov-2002 15:43 779  
[TXT]ACL2-PC_colon__colon_NIL.html13-Nov-2002 15:43 748  
[TXT]ACL2-PC_colon__colon_NOISE.html13-Nov-2002 15:43 1.0K 
[TXT]ACL2-PC_colon__colon_NX.html13-Nov-2002 15:43 1.0K 
[TXT]ACL2-PC_colon__colon_ORELSE.html13-Nov-2002 15:43 886  
[TXT]ACL2-PC_colon__colon_P-TOP.html13-Nov-2002 15:43 1.3K 
[TXT]ACL2-PC_colon__colon_P.html13-Nov-2002 15:43 1.0K 
[TXT]ACL2-PC_colon__colon_PP.html13-Nov-2002 15:43 730  
[TXT]ACL2-PC_colon__colon_PRINT-ALL-CONCS.html13-Nov-2002 15:43 659  
[TXT]ACL2-PC_colon__colon_PRINT-ALL-GOALS.html13-Nov-2002 15:43 629  
[TXT]ACL2-PC_colon__colon_PRINT-MAIN.html13-Nov-2002 15:43 519  
[TXT]ACL2-PC_colon__colon_PRINT.html13-Nov-2002 15:43 1.1K 
[TXT]ACL2-PC_colon__colon_PRO.html13-Nov-2002 15:43 697  
[TXT]ACL2-PC_colon__colon_PROMOTE.html13-Nov-2002 15:43 1.4K 
[TXT]ACL2-PC_colon__colon_PROTECT.html13-Nov-2002 15:43 947  
[TXT]ACL2-PC_colon__colon_PROVE.html13-Nov-2002 15:43 1.6K 
[TXT]ACL2-PC_colon__colon_PUT.html13-Nov-2002 15:43 1.9K 
[TXT]ACL2-PC_colon__colon_QUIET.html13-Nov-2002 15:43 633  
[TXT]ACL2-PC_colon__colon_R.html13-Nov-2002 15:43 716  
[TXT]ACL2-PC_colon__colon_REDUCE-BY-INDUCTION.html13-Nov-2002 15:43 1.4K 
[TXT]ACL2-PC_colon__colon_REDUCE.html13-Nov-2002 15:43 1.1K 
[TXT]ACL2-PC_colon__colon_REMOVE-ABBREVIATIONS.html13-Nov-2002 15:43 1.3K 
[TXT]ACL2-PC_colon__colon_REPEAT-REC.html13-Nov-2002 15:43 481  
[TXT]ACL2-PC_colon__colon_REPEAT.html13-Nov-2002 15:43 789  
[TXT]ACL2-PC_colon__colon_REPLAY.html13-Nov-2002 15:43 1.5K 
[TXT]ACL2-PC_colon__colon_RESTORE.html13-Nov-2002 15:43 1.2K 
[TXT]ACL2-PC_colon__colon_RETAIN.html13-Nov-2002 15:43 851  
[TXT]ACL2-PC_colon__colon_RETRIEVE.html13-Nov-2002 15:43 1.2K 
[TXT]ACL2-PC_colon__colon_REWRITE.html13-Nov-2002 15:43 5.5K 
[TXT]ACL2-PC_colon__colon_RUN-INSTR-ON-GOAL.html13-Nov-2002 15:43 478  
[TXT]ACL2-PC_colon__colon_RUN-INSTR-ON-NEW-GOALS.html13-Nov-2002 15:43 501  
[TXT]ACL2-PC_colon__colon_RUNES.html13-Nov-2002 15:43 655  
[TXT]ACL2-PC_colon__colon_S-PROP.html13-Nov-2002 15:43 913  
[TXT]ACL2-PC_colon__colon_S.html13-Nov-2002 15:43 2.9K 
[TXT]ACL2-PC_colon__colon_SAVE.html13-Nov-2002 15:43 1.2K 
[TXT]ACL2-PC_colon__colon_SEQUENCE.html13-Nov-2002 15:43 4.8K 
[TXT]ACL2-PC_colon__colon_SHOW-ABBREVIATIONS.html13-Nov-2002 15:43 1.5K 
[TXT]ACL2-PC_colon__colon_SHOW-REWRITES.html13-Nov-2002 15:43 1.4K 
[TXT]ACL2-PC_colon__colon_SKIP.html13-Nov-2002 15:43 563  
[TXT]ACL2-PC_colon__colon_SL.html13-Nov-2002 15:43 854  
[TXT]ACL2-PC_colon__colon_SPLIT.html13-Nov-2002 15:43 1.8K 
[TXT]ACL2-PC_colon__colon_SR.html13-Nov-2002 15:43 597  
[TXT]ACL2-PC_colon__colon_SUCCEED.html13-Nov-2002 15:43 727  
[TXT]ACL2-PC_colon__colon_TH.html13-Nov-2002 15:43 1.2K 
[TXT]ACL2-PC_colon__colon_THEN.html13-Nov-2002 15:43 962  
[TXT]ACL2-PC_colon__colon_TOP.html13-Nov-2002 15:43 1.0K 
[TXT]ACL2-PC_colon__colon_TYPE-ALIST.html13-Nov-2002 15:43 618  
[TXT]ACL2-PC_colon__colon_UNDO.html13-Nov-2002 15:43 1.2K 
[TXT]ACL2-PC_colon__colon_UNSAVE.html13-Nov-2002 15:43 1.0K 
[TXT]ACL2-PC_colon__colon_UP.html13-Nov-2002 15:43 1.1K 
[TXT]ACL2-PC_colon__colon_USE.html13-Nov-2002 15:43 1.1K 
[TXT]ACL2-PC_colon__colon_X-DUMB.html13-Nov-2002 15:43 772  
[TXT]ACL2-PC_colon__colon_X.html13-Nov-2002 15:43 2.5K 
[TXT]ACL2-TUTORIAL.html13-Nov-2002 15:42 1.8K 
[TXT]ACL2-USER.html13-Nov-2002 15:43 2.8K 
[TXT]ACL2_Characters.html13-Nov-2002 15:43 1.2K 
[TXT]ACL2_Conses_or_Ordered_Pairs.html13-Nov-2002 15:43 2.1K 
[TXT]ACL2_Strings.html13-Nov-2002 15:43 1.2K 
[TXT]ACL2_Symbols.html13-Nov-2002 15:43 3.3K 
[TXT]ACL2_System_Architecture.html13-Nov-2002 15:43 1.0K 
[TXT]ACL2_as_an_Interactive_Theorem_Prover.html13-Nov-2002 15:43 731  
[TXT]ACL2_as_an_Interactive_Theorem_Prover__lparen_continued_rparen_.html13-Nov-2002 15:43 972  
[TXT]ACL2_is_an_Untyped_Language.html13-Nov-2002 15:43 1.4K 
[TXT]ACONS.html13-Nov-2002 15:43 723  
[TXT]ADD-BINOP.html13-Nov-2002 15:43 1.5K 
[TXT]ADD-INVISIBLE-FNS.html13-Nov-2002 15:43 1.4K 
[TXT]ADD-MACRO-ALIAS.html13-Nov-2002 15:43 1.2K 
[TXT]ADD-MATCH-FREE-OVERRIDE.html13-Nov-2002 15:43 5.0K 
[TXT]ADD-NTH-ALIAS.html13-Nov-2002 15:43 1.0K 
[TXT]ADD-TO-SET-EQ.html13-Nov-2002 15:43 872  
[TXT]ADD-TO-SET-EQL.html13-Nov-2002 15:43 874  
[TXT]ALISTP.html13-Nov-2002 15:43 557  
[TXT]ALLOCATE-FIXNUM-RANGE.html13-Nov-2002 15:43 1.1K 
[TXT]ALPHA-CHAR-P.html13-Nov-2002 15:43 854  
[TXT]ALPHORDER.html13-Nov-2002 15:43 1.4K 
[TXT]AND.html13-Nov-2002 15:43 719  
[TXT]APPEND.html13-Nov-2002 15:43 885  
[TXT]APROPOS.html13-Nov-2002 15:43 1.2K 
[TXT]AREF1.html13-Nov-2002 15:43 1.2K 
[TXT]AREF2.html13-Nov-2002 15:43 1.2K 
[TXT]ARGS.html13-Nov-2002 15:43 1.0K 
[TXT]ARRAY1P.html13-Nov-2002 15:43 774  
[TXT]ARRAY2P.html13-Nov-2002 15:43 774  
[TXT]ARRAYS-EXAMPLE.html13-Nov-2002 15:43 2.8K 
[TXT]ARRAYS.html13-Nov-2002 15:43 27K 
[TXT]ASET1.html13-Nov-2002 15:43 2.4K 
[TXT]ASET2.html13-Nov-2002 15:43 2.5K 
[TXT]ASH.html13-Nov-2002 15:43 953  
[TXT]ASSIGN.html13-Nov-2002 15:43 1.6K 
[TXT]ASSOC-EQ.html13-Nov-2002 15:43 1.2K 
[TXT]ASSOC-EQUAL.html13-Nov-2002 15:43 1.2K 
[TXT]ASSOC-KEYWORD.html13-Nov-2002 15:43 846  
[TXT]ASSOC-STRING-EQUAL.html13-Nov-2002 15:43 918  
[TXT]ASSOC.html13-Nov-2002 15:43 1.9K 
[TXT]ATOM-LISTP.html13-Nov-2002 15:43 568  
[TXT]ATOM.html13-Nov-2002 15:43 631  
[TXT]A_Flying_Tour_of_ACL2.html13-Nov-2002 15:43 1.9K 
[TXT]A_Sketch_of_How_the_Rewriter_Works.html13-Nov-2002 15:43 1.3K 
[TXT]A_Tiny_Warning_Sign.html13-Nov-2002 15:43 821  
[TXT]A_Trivial_Proof.html13-Nov-2002 15:43 298  
[TXT]A_Typical_State.html13-Nov-2002 15:43 1.0K 
[TXT]A_Walking_Tour_of_ACL2.html13-Nov-2002 15:43 1.3K 
[TXT]About_Models.html13-Nov-2002 15:43 940  
[TXT]About_Types.html13-Nov-2002 15:43 2.8K 
[TXT]About_the_ACL2_Home_Page.html13-Nov-2002 15:43 1.9K 
[TXT]About_the_Admission_of_Recursive_Definitions.html13-Nov-2002 15:43 1.9K 
[TXT]About_the_Prompt.html13-Nov-2002 15:43 3.8K 
[TXT]An_Example_Common_Lisp_Function_Definition.html13-Nov-2002 15:43 1.6K 
[TXT]An_Example_of_ACL2_in_Use.html13-Nov-2002 15:43 1.5K 
[TXT]Analyzing_Common_Lisp_Models.html13-Nov-2002 15:43 1.5K 
[TXT]BACKCHAIN-LIMIT.html13-Nov-2002 15:43 5.9K 
[TXT]BDD-ALGORITHM.html13-Nov-2002 15:43 29K 
[TXT]BDD-INTRODUCTION.html13-Nov-2002 15:43 8.3K 
[TXT]BDD.html13-Nov-2002 15:43 2.2K 
[TXT]BIBLIOGRAPHY.html13-Nov-2002 15:43 545  
[TXT]BINARY-+.html13-Nov-2002 15:43 922  
[TXT]BINARY-APPEND.html13-Nov-2002 15:43 686  
[TXT]BINARY-_star_.html13-Nov-2002 15:43 895  
[TXT]BIND-FREE-EXAMPLES.html13-Nov-2002 15:43 6.6K 
[TXT]BIND-FREE.html13-Nov-2002 15:43 11K 
[TXT]BINOP-TABLE.html13-Nov-2002 15:43 806  
[TXT]BOOK-CONTENTS.html13-Nov-2002 15:43 4.3K 
[TXT]BOOK-EXAMPLE.html13-Nov-2002 15:43 11K 
[TXT]BOOK-NAME.html13-Nov-2002 15:43 5.2K 
[TXT]BOOKS.html13-Nov-2002 15:43 4.9K 
[TXT]BOOLEANP.html13-Nov-2002 15:43 698  
[TXT]BREAK-LEMMA.html13-Nov-2002 15:43 5.0K 
[TXT]BREAK-REWRITE.html13-Nov-2002 15:43 16K 
[TXT]BREAKS.html13-Nov-2002 15:43 1.8K 
[TXT]BRR-COMMANDS.html13-Nov-2002 15:43 2.5K 
[TXT]BRR.html13-Nov-2002 15:43 2.7K 
[TXT]BRR_at_.html13-Nov-2002 15:43 5.7K 
[TXT]BUILT-IN-CLAUSES.html13-Nov-2002 15:43 6.0K 
[TXT]BUTLAST.html13-Nov-2002 15:43 1.3K 
[TXT]CAAAAR.html13-Nov-2002 15:43 459  
[TXT]CAAADR.html13-Nov-2002 15:43 459  
[TXT]CAAAR.html13-Nov-2002 15:43 455  
[TXT]CAADAR.html13-Nov-2002 15:43 459  
[TXT]CAADDR.html13-Nov-2002 15:43 459  
[TXT]CAADR.html13-Nov-2002 15:43 455  
[TXT]CAAR.html13-Nov-2002 15:43 451  
[TXT]CADAAR.html13-Nov-2002 15:43 459  
[TXT]CADADR.html13-Nov-2002 15:43 459  
[TXT]CADAR.html13-Nov-2002 15:43 455  
[TXT]CADDAR.html13-Nov-2002 15:43 459  
[TXT]CADDDR.html13-Nov-2002 15:43 459  
[TXT]CADDR.html13-Nov-2002 15:43 455  
[TXT]CADR.html13-Nov-2002 15:43 451  
[TXT]CAR.html13-Nov-2002 15:43 688  
[TXT]CASE-MATCH.html13-Nov-2002 15:43 3.5K 
[TXT]CASE-SPLIT-LIMITATIONS.html13-Nov-2002 15:43 1.0K 
[TXT]CASE-SPLIT.html13-Nov-2002 15:43 2.3K 
[TXT]CASE.html13-Nov-2002 15:43 1.4K 
[TXT]CBD.html13-Nov-2002 15:43 6.3K 
[TXT]CDAAAR.html13-Nov-2002 15:43 459  
[TXT]CDAADR.html13-Nov-2002 15:43 459  
[TXT]CDAAR.html13-Nov-2002 15:43 455  
[TXT]CDADAR.html13-Nov-2002 15:43 459  
[TXT]CDADDR.html13-Nov-2002 15:43 459  
[TXT]CDADR.html13-Nov-2002 15:43 455  
[TXT]CDAR.html13-Nov-2002 15:43 451  
[TXT]CDDAAR.html13-Nov-2002 15:43 459  
[TXT]CDDADR.html13-Nov-2002 15:43 459  
[TXT]CDDAR.html13-Nov-2002 15:43 455  
[TXT]CDDDAR.html13-Nov-2002 15:43 459  
[TXT]CDDDDR.html13-Nov-2002 15:43 459  
[TXT]CDDDR.html13-Nov-2002 15:43 455  
[TXT]CDDR.html13-Nov-2002 15:43 451  
[TXT]CDR.html13-Nov-2002 15:43 721  
[TXT]CEILING.html13-Nov-2002 15:43 1.2K 
[TXT]CERTIFICATE.html13-Nov-2002 15:43 5.4K 
[TXT]CERTIFY-BOOK.html13-Nov-2002 15:43 9.8K 
[TXT]CERTIFY-BOOK_bang_.html13-Nov-2002 15:43 1.5K 
[TXT]CHAR-CODE.html13-Nov-2002 15:43 633  
[TXT]CHAR-DOWNCASE.html13-Nov-2002 15:43 1.0K 
[TXT]CHAR-EQUAL.html13-Nov-2002 15:43 900  
[TXT]CHAR-UPCASE.html13-Nov-2002 15:43 1.0K 
[TXT]CHAR.html13-Nov-2002 15:43 879  
[TXT]CHARACTER-LISTP.html13-Nov-2002 15:43 510  
[TXT]CHARACTERP.html13-Nov-2002 15:43 467  
[TXT]CHARACTERS.html13-Nov-2002 15:43 3.3K 
[TXT]CHAR_gt_.html13-Nov-2002 15:43 806  
[TXT]CHAR_gt_=.html13-Nov-2002 15:43 832  
[TXT]CHAR_lt_.html13-Nov-2002 15:43 800  
[TXT]CHAR_lt_=.html13-Nov-2002 15:43 826  
[TXT]CHECK-SUM.html13-Nov-2002 15:43 2.3K 
[TXT]CHECKPOINT-FORCED-GOALS.html13-Nov-2002 15:43 1.0K 
[TXT]CHECKPOINTS.html13-Nov-2002 15:43 1.2K 
[TXT]CLAUSE-IDENTIFIER.html13-Nov-2002 15:43 2.3K 
[TXT]CLOSE-TRACE-FILE.html13-Nov-2002 15:43 840  
[TXT]CODE-CHAR.html13-Nov-2002 15:43 850  
[TXT]COERCE.html13-Nov-2002 15:43 780  
[TXT]COMMAND-DESCRIPTOR.html13-Nov-2002 15:43 5.0K 
[TXT]COMMAND.html13-Nov-2002 15:43 1.5K 
[TXT]COMP-GCL.html13-Nov-2002 15:43 1.0K 
[TXT]COMP.html13-Nov-2002 15:43 1.7K 
[TXT]COMPILATION.html13-Nov-2002 15:43 521  
[TXT]COMPLEX-RATIONALP.html13-Nov-2002 15:43 730  
[TXT]COMPLEX.html13-Nov-2002 15:43 1.9K 
[TXT]COMPLEX_slash_COMPLEX-RATIONALP.html13-Nov-2002 15:43 1.0K 
[TXT]COMPOUND-RECOGNIZER.html13-Nov-2002 15:43 8.9K 
[TXT]COMPRESS1.html13-Nov-2002 15:43 2.0K 
[TXT]COMPRESS2.html13-Nov-2002 15:43 2.1K 
[TXT]COMPUTED-HINTS.html13-Nov-2002 15:43 5.9K 
[TXT]CONCATENATE.html13-Nov-2002 15:43 1.7K 
[TXT]COND.html13-Nov-2002 15:43 685  
[TXT]CONGRUENCE.html13-Nov-2002 15:43 4.9K 
[TXT]CONJUGATE.html13-Nov-2002 15:43 604  
[TXT]CONS.html13-Nov-2002 15:43 585  
[TXT]CONSP.html13-Nov-2002 15:43 470  
[TXT]CONSTRAINT.html13-Nov-2002 15:43 21K 
[TXT]COPYRIGHT.html13-Nov-2002 15:43 1.6K 
[TXT]COROLLARY.html13-Nov-2002 15:43 653  
[TXT]CURRENT-PACKAGE.html13-Nov-2002 15:43 3.2K 
[TXT]CURRENT-THEORY.html13-Nov-2002 15:43 2.5K 
[TXT]CW-GSTACK.html13-Nov-2002 15:43 3.1K 
[TXT]CW.html13-Nov-2002 15:43 2.4K 
[TXT]Common_Lisp.html13-Nov-2002 15:43 2.1K 
[TXT]Common_Lisp_as_a_Modeling_Language.html13-Nov-2002 15:43 1.7K 
[TXT]Conversion.html13-Nov-2002 15:43 962  
[TXT]Corroborating_Models.html13-Nov-2002 15:43 2.1K 
[TXT]DECLARE-STOBJS.html13-Nov-2002 15:43 2.6K 
[TXT]DECLARE.html13-Nov-2002 15:43 2.0K 
[TXT]DEFABBREV.html13-Nov-2002 15:43 4.2K 
[TXT]DEFAULT-BACKCHAIN-LIMIT.html13-Nov-2002 15:43 508  
[TXT]DEFAULT-DEFUN-MODE.html13-Nov-2002 15:43 3.5K 
[TXT]DEFAULT-HINTS.html13-Nov-2002 15:43 856  
[TXT]DEFAULT-PRINT-PROMPT.html13-Nov-2002 15:43 2.2K 
[TXT]DEFAULT.html13-Nov-2002 15:43 1.2K 
[TXT]DEFAXIOM.html13-Nov-2002 15:43 1.8K 
[TXT]DEFCHOOSE.html13-Nov-2002 15:43 3.8K 
[TXT]DEFCONG.html13-Nov-2002 15:43 2.2K 
[TXT]DEFCONST.html13-Nov-2002 15:43 1.2K 
[TXT]DEFDOC.html13-Nov-2002 15:43 4.3K 
[TXT]DEFEQUIV.html13-Nov-2002 15:43 1.8K 
[TXT]DEFEVALUATOR.html13-Nov-2002 15:43 4.3K 
[TXT]DEFINE-PC-HELP.html13-Nov-2002 15:43 1.5K 
[TXT]DEFINE-PC-MACRO.html13-Nov-2002 15:43 2.0K 
[TXT]DEFINE-PC-META.html13-Nov-2002 15:43 835  
[TXT]DEFINITION.html13-Nov-2002 15:43 8.2K 
[TXT]DEFLABEL.html13-Nov-2002 15:43 1.7K 
[TXT]DEFMACRO.html13-Nov-2002 15:43 3.4K 
[TXT]DEFPKG.html13-Nov-2002 15:43 4.6K 
[TXT]DEFREFINEMENT.html13-Nov-2002 15:43 1.6K 
[TXT]DEFSTOBJ.html13-Nov-2002 15:43 17K 
[TXT]DEFSTUB.html13-Nov-2002 15:43 2.2K 
[TXT]DEFTHEORY.html13-Nov-2002 15:43 1.5K 
[TXT]DEFTHM.html13-Nov-2002 15:43 3.1K 
[TXT]DEFTHMD.html13-Nov-2002 15:43 1.3K 
[TXT]DEFUN-MODE-CAVEAT.html13-Nov-2002 15:43 5.5K 
[TXT]DEFUN-MODE.html13-Nov-2002 15:43 8.1K 
[TXT]DEFUN-SK.html13-Nov-2002 15:43 10K 
[TXT]DEFUN.html13-Nov-2002 15:43 13K 
[TXT]DEFUND.html13-Nov-2002 15:43 1.5K 
[TXT]DEFUNS.html13-Nov-2002 15:43 1.5K 
[TXT]DENOMINATOR.html13-Nov-2002 15:43 581  
[TXT]DIGIT-CHAR-P.html13-Nov-2002 15:43 1.1K 
[TXT]DIGIT-TO-CHAR.html13-Nov-2002 15:43 694  
[TXT]DIMENSIONS.html13-Nov-2002 15:43 1.4K 
[TXT]DISABLE-FORCING.html13-Nov-2002 15:43 1.0K 
[TXT]DISABLE-IMMEDIATE-FORCE-MODEP.html13-Nov-2002 15:43 1.2K 
[TXT]DISABLE.html13-Nov-2002 15:43 1.2K 
[TXT]DISABLEDP.html13-Nov-2002 15:43 1.2K 
[TXT]DOC-STRING.html13-Nov-2002 15:43 16K 
[TXT]DOC.html13-Nov-2002 15:43 3.6K 
[TXT]DOCS.html13-Nov-2002 15:43 1.8K 
[TXT]DOCUMENTATION.html13-Nov-2002 15:43 8.6K 
[TXT]DOC_bang_.html13-Nov-2002 15:43 778  
[TXT]E0-ORD-_lt_.html13-Nov-2002 15:43 4.2K 
[TXT]E0-ORDINALP.html13-Nov-2002 15:43 6.9K 
[TXT]EIGHTH.html13-Nov-2002 15:43 394  
[TXT]ELIM.html13-Nov-2002 15:43 3.4K 
[TXT]EMBEDDED-EVENT-FORM.html13-Nov-2002 15:43 6.3K 
[TXT]ENABLE-FORCING.html13-Nov-2002 15:43 1.1K 
[TXT]ENABLE-IMMEDIATE-FORCE-MODEP.html13-Nov-2002 15:43 1.2K 
[TXT]ENABLE.html13-Nov-2002 15:43 1.2K 
[TXT]ENCAPSULATE.html13-Nov-2002 15:43 8.9K 
[TXT]ENDP.html13-Nov-2002 15:43 1.0K 
[TXT]ENTER-BOOT-STRAP-MODE.html13-Nov-2002 15:43 1.9K 
[TXT]EQ.html13-Nov-2002 15:43 1.4K 
[TXT]EQL.html13-Nov-2002 15:43 1.0K 
[TXT]EQLABLE-ALISTP.html13-Nov-2002 15:43 770  
[TXT]EQLABLE-LISTP.html13-Nov-2002 15:43 631  
[TXT]EQLABLEP.html13-Nov-2002 15:43 715  
[TXT]EQUAL.html13-Nov-2002 15:43 607  
[TXT]EQUIVALENCE.html13-Nov-2002 15:43 10K 
[TXT]ER-PROGN.html13-Nov-2002 15:43 1.3K 
[TXT]ESCAPE-TO-COMMON-LISP.html13-Nov-2002 15:43 798  
[TXT]EVENP.html13-Nov-2002 15:43 747  
[TXT]EVENTS.html13-Nov-2002 15:43 9.8K 
[TXT]EVISCERATE-HIDE-TERMS.html13-Nov-2002 15:43 860  
[TXT]EXECUTABLE-COUNTERPART-THEORY.html13-Nov-2002 15:43 2.0K 
[TXT]EXECUTABLE-COUNTERPART.html13-Nov-2002 15:43 4.7K 
[TXT]EXISTS.html13-Nov-2002 15:43 802  
[TXT]EXIT-BOOT-STRAP-MODE.html13-Nov-2002 15:43 1.2K 
[TXT]EXPLODE-NONNEGATIVE-INTEGER.html13-Nov-2002 15:43 864  
[TXT]EXPT.html13-Nov-2002 15:43 1.0K 
[TXT]EXTENDED-METAFUNCTIONS.html13-Nov-2002 15:43 12K 
[TXT]E_slash_D.html13-Nov-2002 15:43 1.7K 
[TXT]Evaluating_App_on_Sample_Input.html13-Nov-2002 15:43 1.2K 
[TXT]FAILED-FORCING.html13-Nov-2002 15:43 7.8K 
[TXT]FAILURE.html13-Nov-2002 15:43 1.8K 
[TXT]FIFTH.html13-Nov-2002 15:43 391  
[TXT]FILE-READING-EXAMPLE.html13-Nov-2002 15:43 2.5K 
[TXT]FIND-RULES-OF-RUNE.html13-Nov-2002 15:43 1.9K 
[TXT]FIRST.html13-Nov-2002 15:43 391  
[TXT]FIX-TRUE-LIST.html13-Nov-2002 15:43 648  
[TXT]FIX.html13-Nov-2002 15:43 739  
[TXT]FLOOR.html13-Nov-2002 15:43 1.2K 
[TXT]FMS.html13-Nov-2002 15:43 2.7K 
[TXT]FMS_bang_.html13-Nov-2002 15:43 732  
[TXT]FMT-TO-COMMENT-WINDOW.html13-Nov-2002 15:43 1.0K 
[TXT]FMT.html13-Nov-2002 15:43 19K 
[TXT]FMT1.html13-Nov-2002 15:43 2.7K 
[TXT]FMT1_bang_.html13-Nov-2002 15:43 739  
[TXT]FMT_bang_.html13-Nov-2002 15:43 732  
[TXT]FORALL.html13-Nov-2002 15:43 798  
[TXT]FORCE.html13-Nov-2002 15:43 7.5K 
[TXT]FORCING-ROUND.html13-Nov-2002 15:43 8.3K 
[TXT]FORWARD-CHAINING.html13-Nov-2002 15:43 4.7K 
[TXT]FOURTH.html13-Nov-2002 15:43 394  
[TXT]FREE-VARIABLES-EXAMPLES.html13-Nov-2002 15:43 7.0K 
[TXT]FREE-VARIABLES.html13-Nov-2002 15:43 13K 
[TXT]FULL-BOOK-NAME.html13-Nov-2002 15:43 2.1K 
[TXT]FUNCTION-THEORY.html13-Nov-2002 15:43 1.9K 
[TXT]FUNCTIONAL-INSTANTIATION-EXAMPLE.html13-Nov-2002 15:43 3.6K 
[TXT]Flawed_Induction_Candidates_in_App_Example.html13-Nov-2002 15:43 837  
[TXT]Free_Variables_in_Top-Level_Input.html13-Nov-2002 15:43 2.1K 
[TXT]Functions_for_Manipulating_these_Objects.html13-Nov-2002 15:43 1.3K 
[TXT]GC$.html13-Nov-2002 15:43 878  
[TXT]GENERALIZE.html13-Nov-2002 15:43 1.3K 
[TXT]GENERALIZED-BOOLEANS.html13-Nov-2002 15:43 4.4K 
[TXT]GOAL-SPEC.html13-Nov-2002 15:43 3.5K 
[TXT]GOOD-BYE.html13-Nov-2002 15:43 1.2K 
[TXT]GROUND-ZERO.html13-Nov-2002 15:43 928  
[TXT]GUARD-EXAMPLE.html13-Nov-2002 15:43 9.1K 
[TXT]GUARD-INTRODUCTION.html13-Nov-2002 15:43 2.9K 
[TXT]GUARD-MISCELLANY.html13-Nov-2002 15:43 4.5K 
[TXT]GUARD-QUICK-REFERENCE.html13-Nov-2002 15:43 3.9K 
[TXT]GUARD.html13-Nov-2002 15:43 2.5K 
[TXT]GUARDS-AND-EVALUATION.html13-Nov-2002 15:43 16K 
[TXT]GUARDS-FOR-SPECIFICATION.html13-Nov-2002 15:43 2.6K 
[TXT]Guards.html13-Nov-2002 15:43 2.0K 
[TXT]Guessing_the_Type_of_a_Newly_Admitted_Function.html13-Nov-2002 15:43 1.2K 
[TXT]Guiding_the_ACL2_Theorem_Prover.html13-Nov-2002 15:43 769  
[TXT]HARD-ERROR.html13-Nov-2002 15:43 1.8K 
[TXT]HELP.html13-Nov-2002 15:43 520  
[TXT]HIDE.html13-Nov-2002 15:43 5.1K 
[TXT]HINTS.html13-Nov-2002 15:43 20K 
[TXT]HISTORY.html13-Nov-2002 15:43 4.0K 
[TXT]Hey_Wait_bang___Is_ACL2_Typed_or_Untyped_lparen_Q_rparen_.html13-Nov-2002 15:43 1.2K 
[TXT]How_Long_Does_It_Take_to_Become_an_Effective_User_lparen_Q_rparen_.html13-Nov-2002 15:43 1.3K 
[TXT]How_To_Find_Out_about_ACL2_Functions.html13-Nov-2002 15:43 1.7K 
[TXT]How_To_Find_Out_about_ACL2_Functions__lparen_continued_rparen_.html13-Nov-2002 15:43 1.6K 
[TXT]I-AM-HERE.html13-Nov-2002 15:43 1.3K 
[TXT]I-CLOSE.html13-Nov-2002 15:43 545  
[TXT]I-LARGE.html13-Nov-2002 15:43 560  
[TXT]I-LIMITED.html13-Nov-2002 15:43 538  
[TXT]I-SMALL.html13-Nov-2002 15:43 537  
[TXT]IDENTITY.html13-Nov-2002 15:43 523  
[TXT]IF.html13-Nov-2002 15:43 791  
[TXT]IFF.html13-Nov-2002 15:43 565  
[TXT]IFIX.html13-Nov-2002 15:43 788  
[TXT]IF_star_.html13-Nov-2002 15:43 8.2K 
[TXT]ILLEGAL.html13-Nov-2002 15:43 1.4K 
[TXT]IMAGPART.html13-Nov-2002 15:43 572  
[TXT]IMMEDIATE-FORCE-MODEP.html13-Nov-2002 15:43 1.8K 
[TXT]IMPLIES.html13-Nov-2002 15:43 549  
[TXT]IMPROPER-CONSP.html13-Nov-2002 15:43 642  
[TXT]IN-ARITHMETIC-THEORY.html13-Nov-2002 15:43 2.8K 
[TXT]IN-PACKAGE.html13-Nov-2002 15:43 1.0K 
[TXT]IN-THEORY.html13-Nov-2002 15:43 2.1K 
[TXT]INCLUDE-BOOK.html13-Nov-2002 15:43 8.4K 
[TXT]INCOMPATIBLE.html13-Nov-2002 15:43 954  
[TXT]INDUCTION.html13-Nov-2002 15:43 9.5K 
[TXT]INSTRUCTIONS.html13-Nov-2002 15:43 1.3K 
[TXT]INT=.html13-Nov-2002 15:43 787  
[TXT]INTEGER-LENGTH.html13-Nov-2002 15:43 865  
[TXT]INTEGER-LISTP.html13-Nov-2002 15:43 470  
[TXT]INTEGERP.html13-Nov-2002 15:43 433  
[TXT]INTERN-IN-PACKAGE-OF-SYMBOL.html13-Nov-2002 15:43 2.9K 
[TXT]INTERN.html13-Nov-2002 15:43 2.2K 
[TXT]INTERSECTION-THEORIES.html13-Nov-2002 15:43 1.3K 
[TXT]INTERSECTP-EQ.html13-Nov-2002 15:43 605  
[TXT]INTERSECTP-EQUAL.html13-Nov-2002 15:43 926  
[TXT]INTRODUCTION.html13-Nov-2002 15:42 32K 
[TXT]INVISIBLE-FNS-TABLE.html13-Nov-2002 15:43 2.7K 
[TXT]IO.html13-Nov-2002 15:43 7.0K 
[TXT]IRRELEVANT-FORMALS.html13-Nov-2002 15:43 3.9K 
[TXT]KEEP.html13-Nov-2002 15:43 2.0K 
[TXT]KEYWORD-COMMANDS.html13-Nov-2002 15:43 1.7K 
[TXT]KEYWORD-VALUE-LISTP.html13-Nov-2002 15:43 606  
[TXT]KEYWORDP.html13-Nov-2002 15:43 796  
[TXT]LAST.html13-Nov-2002 15:43 950  
[TXT]LD-ERROR-ACTION.html13-Nov-2002 15:43 2.3K 
[TXT]LD-ERROR-TRIPLES.html13-Nov-2002 15:43 1.8K 
[TXT]LD-EVISC-TUPLE.html13-Nov-2002 15:43 2.4K 
[TXT]LD-KEYWORD-ALIASES.html13-Nov-2002 15:43 3.1K 
[TXT]LD-POST-EVAL-PRINT.html13-Nov-2002 15:43 4.6K 
[TXT]LD-PRE-EVAL-FILTER.html13-Nov-2002 15:43 2.1K 
[TXT]LD-PRE-EVAL-PRINT.html13-Nov-2002 15:43 2.8K 
[TXT]LD-PROMPT.html13-Nov-2002 15:43 3.2K 
[TXT]LD-QUERY-CONTROL-ALIST.html13-Nov-2002 15:43 3.8K 
[TXT]LD-REDEFINITION-ACTION.html13-Nov-2002 15:43 10K 
[TXT]LD-SKIP-PROOFSP.html13-Nov-2002 15:43 7.7K 
[TXT]LD-VERBOSE.html13-Nov-2002 15:43 2.3K 
[TXT]LD.html13-Nov-2002 15:43 15K 
[TXT]LEMMA-INSTANCE.html13-Nov-2002 15:43 5.4K 
[TXT]LEN.html13-Nov-2002 15:43 568  
[TXT]LENGTH.html13-Nov-2002 15:43 652  
[TXT]LET.html13-Nov-2002 15:43 6.9K 
[TXT]LET_star_.html13-Nov-2002 15:43 1.5K 
[TXT]LEXORDER.html13-Nov-2002 15:43 1.2K 
[TXT]LICENSE13-Nov-2002 15:42 18K 
[TXT]LINEAR-ARITHMETIC.html13-Nov-2002 15:43 4.2K 
[TXT]LINEAR.html13-Nov-2002 15:43 8.7K 
[TXT]LIST.html13-Nov-2002 15:43 692  
[TXT]LISTP.html13-Nov-2002 15:43 723  
[TXT]LIST_star_.html13-Nov-2002 15:43 677  
[TXT]LOCAL-INCOMPATIBILITY.html13-Nov-2002 15:43 5.7K 
[TXT]LOCAL.html13-Nov-2002 15:43 2.7K 
[TXT]LOGAND.html13-Nov-2002 15:43 931  
[TXT]LOGANDC1.html13-Nov-2002 15:43 771  
[TXT]LOGANDC2.html13-Nov-2002 15:43 772  
[TXT]LOGBITP.html13-Nov-2002 15:43 811  
[TXT]LOGCOUNT.html13-Nov-2002 15:43 691  
[TXT]LOGEQV.html13-Nov-2002 15:43 943  
[TXT]LOGIC.html13-Nov-2002 15:43 1.7K 
[TXT]LOGICAL-NAME.html13-Nov-2002 15:43 4.5K 
[TXT]LOGIOR.html13-Nov-2002 15:43 944  
[TXT]LOGNAND.html13-Nov-2002 15:43 691  
[TXT]LOGNOR.html13-Nov-2002 15:43 711  
[TXT]LOGNOT.html13-Nov-2002 15:43 851  
[TXT]LOGORC1.html13-Nov-2002 15:43 780  
[TXT]LOGORC2.html13-Nov-2002 15:43 781  
[TXT]LOGTEST.html13-Nov-2002 15:43 819  
[TXT]LOGXOR.html13-Nov-2002 15:43 944  
[TXT]LOOP-STOPPER.html13-Nov-2002 15:43 10K 
[TXT]LOWER-CASE-P.html13-Nov-2002 15:43 833  
[TXT]LP.html13-Nov-2002 15:43 4.7K 
[TXT]MACRO-ALIASES-TABLE.html13-Nov-2002 15:43 2.8K 
[TXT]MACRO-ARGS.html13-Nov-2002 15:43 1.9K 
[TXT]MACRO-COMMAND.html13-Nov-2002 15:43 1.7K 
[TXT]MAKE-CHARACTER-LIST.html13-Nov-2002 15:43 505  
[TXT]MAKE-LIST.html13-Nov-2002 15:43 899  
[TXT]MARKUP.html13-Nov-2002 15:43 12K 
[TXT]MAX.html13-Nov-2002 15:43 679  
[TXT]MAXIMUM-LENGTH.html13-Nov-2002 15:43 1.2K 
[TXT]MEMBER-EQ.html13-Nov-2002 15:43 1.1K 
[TXT]MEMBER-EQUAL.html13-Nov-2002 15:43 1.0K 
[TXT]MEMBER.html13-Nov-2002 15:43 1.7K 
[TXT]META.html13-Nov-2002 15:43 15K 
[TXT]MIN.html13-Nov-2002 15:43 681  
[TXT]MINIMAL-THEORY.html13-Nov-2002 15:43 1.4K 
[TXT]MINUSP.html13-Nov-2002 15:43 680  
[TXT]MISCELLANEOUS.html13-Nov-2002 15:43 16K 
[TXT]MOD.html13-Nov-2002 15:43 970  
[TXT]MONITOR.html13-Nov-2002 15:43 10K 
[TXT]MONITORED-RUNES.html13-Nov-2002 15:43 705  
[TXT]MORE-DOC.html13-Nov-2002 15:43 1.5K 
[TXT]MORE.html13-Nov-2002 15:43 2.8K 
[TXT]MORE_bang_.html13-Nov-2002 15:43 1.3K 
[TXT]MUTUAL-RECURSION-PROOF-EXAMPLE.html13-Nov-2002 15:43 5.4K 
[TXT]MUTUAL-RECURSION.html13-Nov-2002 15:43 4.5K 
[TXT]MV-LET.html13-Nov-2002 15:43 5.8K 
[TXT]MV-NTH.html13-Nov-2002 15:43 1.1K 
[TXT]MV.html13-Nov-2002 15:43 1.2K 
[TXT]Modeling_in_ACL2.html13-Nov-2002 15:43 1.0K 
[TXT]Models_in_Engineering.html13-Nov-2002 15:43 827  
[TXT]Models_of_Computer_Hardware_and_Software.html13-Nov-2002 15:43 1.1K 
[TXT]NAME.html13-Nov-2002 15:43 2.5K 
[TXT]NFIX.html13-Nov-2002 15:43 814  
[TXT]NINTH.html13-Nov-2002 15:43 391  
[TXT]NO-DUPLICATESP-EQUAL.html13-Nov-2002 15:43 802  
[TXT]NO-DUPLICATESP.html13-Nov-2002 15:43 763  
[TXT]NON-LINEAR-ARITHMETIC.html13-Nov-2002 15:43 7.7K 
[TXT]NONNEGATIVE-INTEGER-QUOTIENT.html13-Nov-2002 15:43 1.1K 
[TXT]NOT.html13-Nov-2002 15:43 587  
[TXT]NOTE-2-0.html13-Nov-2002 15:43 1.5K 
[TXT]NOTE-2-1.html13-Nov-2002 15:43 693  
[TXT]NOTE-2-2.html13-Nov-2002 15:43 3.2K 
[TXT]NOTE-2-3.html13-Nov-2002 15:43 2.6K 
[TXT]NOTE-2-4.html13-Nov-2002 15:43 2.0K 
[TXT]NOTE-2-5.html13-Nov-2002 15:43 19K 
[TXT]NOTE-2-5_lparen_R_rparen_.html13-Nov-2002 15:43 590  
[TXT]NOTE-2-6-GUARDS.html13-Nov-2002 15:43 4.0K 
[TXT]NOTE-2-6-NEW-FUNCTIONALITY.html13-Nov-2002 15:43 11K 
[TXT]NOTE-2-6-OTHER.html13-Nov-2002 15:43 6.6K 
[TXT]NOTE-2-6-PROOF-CHECKER.html13-Nov-2002 15:43 1.4K 
[TXT]NOTE-2-6-PROOFS.html13-Nov-2002 15:43 6.2K 
[TXT]NOTE-2-6-RULES.html13-Nov-2002 15:43 4.7K 
[TXT]NOTE-2-6-SYSTEM.html13-Nov-2002 15:43 2.7K 
[TXT]NOTE-2-6.html13-Nov-2002 15:43 2.0K 
[TXT]NOTE-2-6_lparen_R_rparen_.html13-Nov-2002 15:43 620  
[TXT]NOTE-2-7-BUG-FIXES.html13-Nov-2002 15:43 17K 
[TXT]NOTE-2-7-GUARDS.html13-Nov-2002 15:43 1.1K 
[TXT]NOTE-2-7-NEW-FUNCTIONALITY.html13-Nov-2002 15:43 10K 
[TXT]NOTE-2-7-OTHER.html13-Nov-2002 15:43 10K 
[TXT]NOTE-2-7-PROOF-CHECKER.html13-Nov-2002 15:43 623  
[TXT]NOTE-2-7-PROOFS.html13-Nov-2002 15:43 6.3K 
[TXT]NOTE-2-7-RULES.html13-Nov-2002 15:43 1.4K 
[TXT]NOTE-2-7-SYSTEM.html13-Nov-2002 15:43 3.5K 
[TXT]NOTE-2-7.html13-Nov-2002 15:43 5.8K 
[TXT]NOTE-2-7_lparen_R_rparen_.html13-Nov-2002 15:43 1.1K 
[TXT]NOTE1.html13-Nov-2002 15:43 1.5K 
[TXT]NOTE2.html13-Nov-2002 15:43 2.3K 
[TXT]NOTE3.html13-Nov-2002 15:43 7.4K 
[TXT]NOTE4.html13-Nov-2002 15:43 9.6K 
[TXT]NOTE5.html13-Nov-2002 15:43 18K 
[TXT]NOTE6.html13-Nov-2002 15:43 7.5K 
[TXT]NOTE7.html13-Nov-2002 15:43 11K 
[TXT]NOTE8-UPDATE.html13-Nov-2002 15:43 3.4K 
[TXT]NOTE8.html13-Nov-2002 15:43 21K 
[TXT]NOTE9.html13-Nov-2002 15:43 3.5K 
[TXT]NQTHM-TO-ACL2.html13-Nov-2002 15:43 7.6K 
[TXT]NTH-ALIASES-TABLE.html13-Nov-2002 15:43 1.6K 
[TXT]NTH.html13-Nov-2002 15:43 854  
[TXT]NTHCDR.html13-Nov-2002 15:43 1.0K 
[TXT]NU-REWRITER.html13-Nov-2002 15:43 826  
[TXT]NULL.html13-Nov-2002 15:43 727  
[TXT]NUMERATOR.html13-Nov-2002 15:43 572  
[TXT]Name_the_Formula_Above.html13-Nov-2002 15:43 415  
[TXT]Nontautological_Subgoals.html13-Nov-2002 15:43 583  
[TXT]Numbers_in_ACL2.html13-Nov-2002 15:43 2.6K 
[TXT]OBDD.html13-Nov-2002 15:43 431  
[TXT]ODDP.html13-Nov-2002 15:43 694  
[TXT]OK-IF.html13-Nov-2002 15:43 2.4K 
[TXT]OOPS.html13-Nov-2002 15:43 5.2K 
[TXT]OPEN-TRACE-FILE.html13-Nov-2002 15:43 1.0K 
[TXT]OR.html13-Nov-2002 15:43 632  
[TXT]OTF-FLG.html13-Nov-2002 15:43 2.3K 
[TXT]OTHER.html13-Nov-2002 15:43 3.1K 
[TXT]On_the_Naming_of_Subgoals.html13-Nov-2002 15:43 613  
[TXT]Other_Requirements.html13-Nov-2002 15:43 1.1K 
[TXT]Overview_of_the_Expansion_of_ENDP_in_the_Base_Case.html13-Nov-2002 15:43 566  
[TXT]Overview_of_the_Expansion_of_ENDP_in_the_Induction_Step.html13-Nov-2002 15:43 800  
[TXT]Overview_of_the_Final_Simplification_in_the_Base_Case.html13-Nov-2002 15:43 540  
[TXT]Overview_of_the_Proof_of_a_Trivial_Consequence.html13-Nov-2002 15:43 1.8K 
[TXT]Overview_of_the_Simplification_of_the_Base_Case_to_T.html13-Nov-2002 15:43 971  
[TXT]Overview_of_the_Simplification_of_the_Induction_Conclusion.html13-Nov-2002 15:43 725  
[TXT]Overview_of_the_Simplification_of_the_Induction_Step_to_T.html13-Nov-2002 15:43 1.2K 
[TXT]PACKAGE-REINCARNATION-IMPORT-RESTRICTIONS.html13-Nov-2002 15:43 2.5K 
[TXT]PAIRLIS$.html13-Nov-2002 15:43 962  
[TXT]PAIRLIS.html13-Nov-2002 15:43 560  
[TXT]PATHNAME.html13-Nov-2002 15:43 2.0K 
[TXT]PBT.html13-Nov-2002 15:43 1.4K 
[TXT]PC.html13-Nov-2002 15:43 7.4K 
[TXT]PCB.html13-Nov-2002 15:43 2.3K 
[TXT]PCB_bang_.html13-Nov-2002 15:43 1.0K 
[TXT]PCS.html13-Nov-2002 15:43 1.2K 
[TXT]PE.html13-Nov-2002 15:43 1.4K 
[TXT]PE_bang_.html13-Nov-2002 15:43 1.4K 
[TXT]PF.html13-Nov-2002 15:43 721  
[TXT]PL.html13-Nov-2002 15:43 950  
[TXT]PLUSP.html13-Nov-2002 15:43 675  
[TXT]PORTCULLIS.html13-Nov-2002 15:43 5.1K 
[TXT]POSITION-EQ.html13-Nov-2002 15:43 1.4K 
[TXT]POSITION-EQUAL.html13-Nov-2002 15:43 1.1K 
[TXT]POSITION.html13-Nov-2002 15:43 1.9K 
[TXT]PPROGN.html13-Nov-2002 15:43 1.4K 
[TXT]PR.html13-Nov-2002 15:43 1.9K 
[TXT]PRINT-CHECKPOINTS.html13-Nov-2002 15:43 675  
[TXT]PRINT-DOC-START-COLUMN.html13-Nov-2002 15:43 1.4K 
[TXT]PROG2$.html13-Nov-2002 15:43 2.8K 
[TXT]PROGN.html13-Nov-2002 15:43 1.1K 
[TXT]PROGRAM.html13-Nov-2002 15:43 1.8K 
[TXT]PROGRAMMING.html13-Nov-2002 15:43 33K 
[TXT]PROMPT.html13-Nov-2002 15:43 581  
[TXT]PROOF-CHECKER-COMMANDS.html13-Nov-2002 15:43 15K 
[TXT]PROOF-CHECKER.html13-Nov-2002 15:43 2.6K 
[TXT]PROOF-OF-WELL-FOUNDEDNESS.html13-Nov-2002 15:43 7.2K 
[TXT]PROOF-TREE-BINDINGS.html13-Nov-2002 15:43 2.8K 
[TXT]PROOF-TREE-DETAILS.html13-Nov-2002 15:43 2.8K 
[TXT]PROOF-TREE-EMACS.html13-Nov-2002 15:43 3.2K 
[TXT]PROOF-TREE-EXAMPLES.html13-Nov-2002 15:43 10K 
[TXT]PROOF-TREE.html13-Nov-2002 15:43 4.6K 
[TXT]PROOFS-CO.html13-Nov-2002 15:43 1.1K 
[TXT]PROPER-CONSP.html13-Nov-2002 15:43 567  
[TXT]PROPS.html13-Nov-2002 15:43 534  
[TXT]PR_bang_.html13-Nov-2002 15:43 1.2K 
[TXT]PSEUDO-TERMP.html13-Nov-2002 15:43 3.9K 
[TXT]PUFF.html13-Nov-2002 15:43 9.3K 
[TXT]PUFF_star_.html13-Nov-2002 15:43 4.1K 
[TXT]PUSH-UNTOUCHABLE.html13-Nov-2002 15:43 1.6K 
[TXT]PUT-ASSOC-EQ.html13-Nov-2002 15:43 1.2K 
[TXT]PUT-ASSOC-EQL.html13-Nov-2002 15:43 1.2K 
[TXT]PUT-ASSOC-EQUAL.html13-Nov-2002 15:43 942  
[TXT]Pages_Written_Especially_for_the_Tours.html13-Nov-2002 15:43 18K 
[TXT]Perhaps.html13-Nov-2002 15:43 376  
[TXT]Popping_out_of_an_Inductive_Proof.html13-Nov-2002 15:43 551  
[TXT]Proving_Theorems_about_Models.html13-Nov-2002 15:43 969  
[TXT]Q.html13-Nov-2002 15:43 1.1K 
[TXT]QUANTIFIERS-USING-DEFUN-SK-EXTENDED.html13-Nov-2002 15:43 2.6K 
[TXT]QUANTIFIERS-USING-DEFUN-SK.html13-Nov-2002 15:43 1.9K 
[TXT]QUANTIFIERS-USING-RECURSION.html13-Nov-2002 15:43 1.1K 
[TXT]QUANTIFIERS.html13-Nov-2002 15:43 2.3K 
[TXT]RASSOC.html13-Nov-2002 15:43 1.2K 
[TXT]RATIONAL-LISTP.html13-Nov-2002 15:43 489  
[TXT]RATIONALP.html13-Nov-2002 15:43 469  
[TXT]REAL-LISTP.html13-Nov-2002 15:43 542  
[TXT]REAL.html13-Nov-2002 15:43 2.8K 
[TXT]REALFIX.html13-Nov-2002 15:43 796  
[TXT]REALPART.html13-Nov-2002 15:43 567  
[TXT]REAL_slash_RATIONALP.html13-Nov-2002 15:43 916  
[TXT]REBUILD.html13-Nov-2002 15:43 3.0K 
[TXT]REDEF.html13-Nov-2002 15:43 1.2K 
[TXT]REDEFINED-NAMES.html13-Nov-2002 15:43 1.1K 
[TXT]REDEFINING-PROGRAMS.html13-Nov-2002 15:43 8.1K 
[TXT]REDEF_bang_.html13-Nov-2002 15:43 959  
[TXT]REDUNDANT-EVENTS.html13-Nov-2002 15:43 6.9K 
[TXT]REFINEMENT.html13-Nov-2002 15:43 2.8K 
[TXT]RELEASE-NOTES.html13-Nov-2002 15:43 2.6K 
[TXT]REM.html13-Nov-2002 15:43 1.0K 
[TXT]REMOVE-BINOP.html13-Nov-2002 15:43 914  
[TXT]REMOVE-DUPLICATES-EQUAL.html13-Nov-2002 15:43 1.0K 
[TXT]REMOVE-DUPLICATES.html13-Nov-2002 15:43 1.4K 
[TXT]REMOVE-INVISIBLE-FNS.html13-Nov-2002 15:43 1.1K 
[TXT]REMOVE-MACRO-ALIAS.html13-Nov-2002 15:43 1.0K 
[TXT]REMOVE-NTH-ALIAS.html13-Nov-2002 15:43 1.0K 
[TXT]REMOVE.html13-Nov-2002 15:43 1.1K 
[TXT]RESET-LD-SPECIALS.html13-Nov-2002 15:43 2.0K 
[TXT]RESIZE-LIST.html13-Nov-2002 15:43 927  
[TXT]REST.html13-Nov-2002 15:43 570  
[TXT]RETRIEVE.html13-Nov-2002 15:43 751  
[TXT]REVAPPEND.html13-Nov-2002 15:43 1.2K 
[TXT]REVERSE.html13-Nov-2002 15:43 687  
[TXT]REWRITE.html13-Nov-2002 15:43 4.9K 
[TXT]RFIX.html13-Nov-2002 15:43 798  
[TXT]ROUND.html13-Nov-2002 15:43 1.2K 
[TXT]RULE-CLASSES.html13-Nov-2002 15:43 19K 
[TXT]RULE-NAMES.html13-Nov-2002 15:43 505  
[TXT]RUNE.html13-Nov-2002 15:43 6.0K 
[TXT]Revisiting_the_Admission_of_App.html13-Nov-2002 15:43 1.8K 
[TXT]Rewrite_Rules_are_Generated_from_DEFTHM_Events.html13-Nov-2002 15:43 1.2K 
[TXT]Running_Models.html13-Nov-2002 15:43 1.1K 
[TXT]SAVING-AND-RESTORING.html13-Nov-2002 15:43 1.5K 
[TXT]SECOND.html13-Nov-2002 15:43 394  
[TXT]SET-BACKCHAIN-LIMIT.html13-Nov-2002 15:43 1.1K 
[TXT]SET-BOGUS-MUTUAL-RECURSION-OK.html13-Nov-2002 15:43 2.1K 
[TXT]SET-CASE-SPLIT-LIMITATIONS.html13-Nov-2002 15:43 6.9K 
[TXT]SET-CBD.html13-Nov-2002 15:43 1.5K 
[TXT]SET-COMPILE-FNS.html13-Nov-2002 15:43 2.6K 
[TXT]SET-DEFAULT-BACKCHAIN-LIMIT.html13-Nov-2002 15:43 1.3K 
[TXT]SET-DEFAULT-HINTS.html13-Nov-2002 15:43 2.5K 
[TXT]SET-DIFFERENCE-EQUAL.html13-Nov-2002 15:43 1.3K 
[TXT]SET-DIFFERENCE-THEORIES.html13-Nov-2002 15:43 1.6K 
[TXT]SET-GUARD-CHECKING.html13-Nov-2002 15:43 3.4K 
[TXT]SET-IGNORE-OK.html13-Nov-2002 15:43 1.5K 
[TXT]SET-INHIBIT-OUTPUT-LST.html13-Nov-2002 15:43 2.2K 
[TXT]SET-INHIBIT-WARNINGS.html13-Nov-2002 15:43 1.5K 
[TXT]SET-INVISIBLE-FNS-TABLE.html13-Nov-2002 15:43 2.1K 
[TXT]SET-IRRELEVANT-FORMALS-OK.html13-Nov-2002 15:43 1.1K 
[TXT]SET-LET_star_-ABSTRACTIONP.html13-Nov-2002 15:43 1.7K 
[TXT]SET-MATCH-FREE-DEFAULT.html13-Nov-2002 15:43 3.1K 
[TXT]SET-MATCH-FREE-ERROR.html13-Nov-2002 15:43 2.7K 
[TXT]SET-MEASURE-FUNCTION.html13-Nov-2002 15:43 1.4K 
[TXT]SET-NON-LINEARP.html13-Nov-2002 15:43 583  
[TXT]SET-NU-REWRITER-MODE.html13-Nov-2002 15:43 2.0K 
[TXT]SET-RAW-MODE.html13-Nov-2002 15:43 5.6K 
[TXT]SET-STATE-OK.html13-Nov-2002 15:43 3.4K 
[TXT]SET-VERIFY-GUARDS-EAGERNESS.html13-Nov-2002 15:43 3.2K 
[TXT]SET-WELL-FOUNDED-RELATION.html13-Nov-2002 15:43 1.9K 
[TXT]SEVENTH.html13-Nov-2002 15:43 397  
[TXT]SHOW-BDD.html13-Nov-2002 15:43 3.0K 
[TXT]SIGNATURE.html13-Nov-2002 15:43 5.1K 
[TXT]SIGNUM.html13-Nov-2002 15:43 1.2K 
[TXT]SIMPLE.html13-Nov-2002 15:43 1.8K 
[TXT]SIXTH.html13-Nov-2002 15:43 391  
[TXT]SKIP-PROOFS.html13-Nov-2002 15:43 5.7K 
[TXT]SLOW-ARRAY-WARNING.html13-Nov-2002 15:43 5.7K 
[TXT]SOLUTION-TO-SIMPLE-EXAMPLE.html13-Nov-2002 15:43 2.6K 
[TXT]SPECIOUS-SIMPLIFICATION.html13-Nov-2002 15:43 6.2K 
[TXT]STANDARD-CHAR-LISTP.html13-Nov-2002 15:43 718  
[TXT]STANDARD-CHAR-P.html13-Nov-2002 15:43 956  
[TXT]STANDARD-CO.html13-Nov-2002 15:43 1.5K 
[TXT]STANDARD-NUMBERP.html13-Nov-2002 15:43 1.1K 
[TXT]STANDARD-OI.html13-Nov-2002 15:43 1.7K 
[TXT]STANDARD-PART.html13-Nov-2002 15:43 687  
[TXT]STANDARD-STRING-ALISTP.html13-Nov-2002 15:43 774  
[TXT]START-PROOF-TREE.html13-Nov-2002 15:43 1.1K 
[TXT]STARTUP.html13-Nov-2002 15:43 3.4K 
[TXT]STATE.html13-Nov-2002 15:43 10K 
[TXT]STOBJ-EXAMPLE-1-DEFUNS.html13-Nov-2002 15:43 5.0K 
[TXT]STOBJ-EXAMPLE-1-IMPLEMENTATION.html13-Nov-2002 15:43 3.4K 
[TXT]STOBJ-EXAMPLE-1-PROOFS.html13-Nov-2002 15:43 6.0K 
[TXT]STOBJ-EXAMPLE-1.html13-Nov-2002 15:43 10K 
[TXT]STOBJ-EXAMPLE-2.html13-Nov-2002 15:43 3.8K 
[TXT]STOBJ-EXAMPLE-3.html13-Nov-2002 15:43 9.6K 
[TXT]STOBJ.html13-Nov-2002 15:43 5.6K 
[TXT]STOP-PROOF-TREE.html13-Nov-2002 15:43 1.1K 
[TXT]STRING-APPEND.html13-Nov-2002 15:43 1.0K 
[TXT]STRING-DOWNCASE.html13-Nov-2002 15:43 874  
[TXT]STRING-EQUAL.html13-Nov-2002 15:43 933  
[TXT]STRING-LISTP.html13-Nov-2002 15:43 509  
[TXT]STRING-UPCASE.html13-Nov-2002 15:43 860  
[TXT]STRING.html13-Nov-2002 15:43 952  
[TXT]STRINGP.html13-Nov-2002 15:43 422  
[TXT]STRING_gt_.html13-Nov-2002 15:43 779  
[TXT]STRING_gt_=.html13-Nov-2002 15:43 1.0K 
[TXT]STRING_lt_.html13-Nov-2002 15:43 1.1K 
[TXT]STRING_lt_=.html13-Nov-2002 15:43 1.0K 
[TXT]STRIP-CARS.html13-Nov-2002 15:43 733  
[TXT]STRIP-CDRS.html13-Nov-2002 15:43 718  
[TXT]SUBLIS.html13-Nov-2002 15:43 1.1K 
[TXT]SUBSEQ.html13-Nov-2002 15:43 1.6K 
[TXT]SUBSETP-EQUAL.html13-Nov-2002 15:43 1.0K 
[TXT]SUBSETP.html13-Nov-2002 15:43 1.2K 
[TXT]SUBST.html13-Nov-2002 15:43 1.0K 
[TXT]SUBSTITUTE.html13-Nov-2002 15:43 1.2K 
[TXT]SUBVERSIVE-INDUCTIONS.html13-Nov-2002 15:43 504  
[TXT]SUBVERSIVE-RECURSIONS.html13-Nov-2002 15:43 6.7K 
[TXT]SYMBOL-ALISTP.html13-Nov-2002 15:43 594  
[TXT]SYMBOL-LISTP.html13-Nov-2002 15:43 465  
[TXT]SYMBOL-NAME.html13-Nov-2002 15:43 575  
[TXT]SYMBOL-PACKAGE-NAME.html13-Nov-2002 15:43 1.0K 
[TXT]SYMBOL-_lt_.html13-Nov-2002 15:43 1.2K 
[TXT]SYMBOLP.html13-Nov-2002 15:43 422  
[TXT]SYNTAX.html13-Nov-2002 15:43 772  
[TXT]SYNTAXP-EXAMPLES.html13-Nov-2002 15:43 7.0K 
[TXT]SYNTAXP.html13-Nov-2002 15:43 8.5K 
[TXT]SYS-CALL-STATUS.html13-Nov-2002 15:43 1.1K 
[TXT]SYS-CALL.html13-Nov-2002 15:43 2.2K 
[TXT]Subsumption_of_Induction_Candidates_in_App_Example.html13-Nov-2002 15:43 749  
[TXT]Suggested_Inductions_in_the_Associativity_of_App_Example.html13-Nov-2002 15:43 824  
[TXT]Symbolic_Execution_of_Models.html13-Nov-2002 15:43 768  
[TXT]TABLE.html13-Nov-2002 15:43 12K 
[TXT]TAKE.html13-Nov-2002 15:43 1.3K 
[TXT]TENTH.html13-Nov-2002 15:43 391  
[TXT]TERM-ORDER.html13-Nov-2002 15:43 7.4K 
[TXT]TERM-TABLE.html13-Nov-2002 15:43 1.5K 
[TXT]TERM.html13-Nov-2002 15:43 11K 
[TXT]THE-METHOD.html13-Nov-2002 15:43 5.1K 
[TXT]THE.html13-Nov-2002 15:43 934  
[TXT]THEORIES.html13-Nov-2002 15:43 11K 
[TXT]THEORY-FUNCTIONS.html13-Nov-2002 15:43 3.8K 
[TXT]THEORY-INVARIANT.html13-Nov-2002 15:43 5.5K 
[TXT]THEORY.html13-Nov-2002 15:43 1.1K 
[TXT]THIRD.html13-Nov-2002 15:43 391  
[TXT]THM.html13-Nov-2002 15:43 1.1K 
[TXT]TIDBITS.html13-Nov-2002 15:43 5.1K 
[TXT]TIPS.html13-Nov-2002 15:43 25K 
[TXT]TOGGLE-PC-MACRO.html13-Nov-2002 15:43 900  
[TXT]TRACE$.html13-Nov-2002 15:43 1.8K 
[TXT]TRACE.html13-Nov-2002 15:43 2.7K 
[TXT]TRANS.html13-Nov-2002 15:43 1.6K 
[TXT]TRANS1.html13-Nov-2002 15:43 740  
[TXT]TRUE-LIST-LISTP.html13-Nov-2002 15:43 628  
[TXT]TRUE-LISTP.html13-Nov-2002 15:43 501  
[TXT]TRUNCATE.html13-Nov-2002 15:43 1.2K 
[TXT]TTREE.html13-Nov-2002 15:43 2.7K 
[TXT]TUTORIAL-EXAMPLES.html13-Nov-2002 15:43 2.8K 
[TXT]TUTORIAL1-TOWERS-OF-HANOI.html13-Nov-2002 15:43 9.4K 
[TXT]TUTORIAL2-EIGHTS-PROBLEM.html13-Nov-2002 15:43 4.6K 
[TXT]TUTORIAL3-PHONEBOOK-EXAMPLE.html13-Nov-2002 15:43 32K 
[TXT]TUTORIAL4-DEFUN-SK-EXAMPLE.html13-Nov-2002 15:43 4.1K 
[TXT]TUTORIAL5-MISCELLANEOUS-EXAMPLES.html13-Nov-2002 15:43 1.1K 
[TXT]TYPE-PRESCRIPTION.html13-Nov-2002 15:43 7.0K 
[TXT]TYPE-SET-INVERTER.html13-Nov-2002 15:43 3.1K 
[TXT]TYPE-SET.html13-Nov-2002 15:43 8.2K 
[TXT]TYPE-SPEC.html13-Nov-2002 15:43 3.0K 
[TXT]The_Admission_of_App.html13-Nov-2002 15:43 1.4K 
[TXT]The_Associativity_of_App.html13-Nov-2002 15:43 1.6K 
[TXT]The_Base_Case_in_the_App_Example.html13-Nov-2002 15:43 692  
[TXT]The_End_of_the_Flying_Tour.html13-Nov-2002 15:43 943  
[TXT]The_End_of_the_Proof_of_the_Associativity_of_App.html13-Nov-2002 15:43 1.0K 
[TXT]The_End_of_the_Walking_Tour.html13-Nov-2002 15:43 778  
[TXT]The_Event_Summary.html13-Nov-2002 15:43 2.9K 
[TXT]The_Expansion_of_ENDP_in_the_Induction_Step__lparen_Step_0_rparen_.html13-Nov-2002 15:43 815  
[TXT]The_Expansion_of_ENDP_in_the_Induction_Step__lparen_Step_1_rparen_.html13-Nov-2002 15:43 845  
[TXT]The_Expansion_of_ENDP_in_the_Induction_Step__lparen_Step_2_rparen_.html13-Nov-2002 15:43 787  
[TXT]The_Falling_Body_Model.html13-Nov-2002 15:43 919  
[TXT]The_Final_Simplification_in_the_Base_Case__lparen_Step_0_rparen_.html13-Nov-2002 15:43 821  
[TXT]The_Final_Simplification_in_the_Base_Case__lparen_Step_1_rparen_.html13-Nov-2002 15:43 744  
[TXT]The_Final_Simplification_in_the_Base_Case__lparen_Step_2_rparen_.html13-Nov-2002 15:43 651  
[TXT]The_Final_Simplification_in_the_Base_Case__lparen_Step_3_rparen_.html13-Nov-2002 15:43 750  
[TXT]The_First_Application_of_the_Associativity_Rule.html13-Nov-2002 15:43 856  
[TXT]The_Induction_Scheme_Selected_for_the_App_Example.html13-Nov-2002 15:43 1.0K 
[TXT]The_Induction_Step_in_the_App_Example.html13-Nov-2002 15:43 1.0K 
[TXT]The_Instantiation_of_the_Induction_Scheme.html13-Nov-2002 15:43 614  
[TXT]The_Justification_of_the_Induction_Scheme.html13-Nov-2002 15:43 496  
[TXT]The_Proof_of_the_Associativity_of_App.html13-Nov-2002 15:43 2.3K 
[TXT]The_Q.E.D._Message.html13-Nov-2002 15:43 426  
[TXT]The_Rules_used_in_the_Associativity_of_App_Proof.html13-Nov-2002 15:43 1.1K 
[TXT]The_Simplification_of_the_Induction_Conclusion__lparen_Step_0_rparen_.html13-Nov-2002 15:43 773  
[TXT]The_Simplification_of_the_Induction_Conclusion__lparen_Step_1_rparen_.html13-Nov-2002 15:43 1.3K 
[TXT]The_Simplification_of_the_Induction_Conclusion__lparen_Step_2_rparen_.html13-Nov-2002 15:43 876  
[TXT]The_Simplification_of_the_Induction_Conclusion__lparen_Step_3_rparen_.html13-Nov-2002 15:43 830  
[TXT]The_Simplification_of_the_Induction_Conclusion__lparen_Step_4_rparen_.html13-Nov-2002 15:43 1.0K 
[TXT]The_Simplification_of_the_Induction_Conclusion__lparen_Step_5_rparen_.html13-Nov-2002 15:43 958  
[TXT]The_Simplification_of_the_Induction_Conclusion__lparen_Step_6_rparen_.html13-Nov-2002 15:43 929  
[TXT]The_Simplification_of_the_Induction_Conclusion__lparen_Step_7_rparen_.html13-Nov-2002 15:43 902  
[TXT]The_Simplification_of_the_Induction_Conclusion__lparen_Step_8_rparen_.html13-Nov-2002 15:43 1.0K 
[TXT]The_Simplification_of_the_Induction_Conclusion__lparen_Step_9_rparen_.html13-Nov-2002 15:43 1.1K 
[TXT]The_Simplification_of_the_Induction_Conclusion__lparen_Step_10_rparen_.html13-Nov-2002 15:43 883  
[TXT]The_Simplification_of_the_Induction_Conclusion__lparen_Step_11_rparen_.html13-Nov-2002 15:43 836  
[TXT]The_Simplification_of_the_Induction_Conclusion__lparen_Step_12_rparen_.html13-Nov-2002 15:43 728  
[TXT]The_Summary_of_the_Proof_of_the_Trivial_Consequence.html13-Nov-2002 15:43 522  
[TXT]The_Theorem_that_App_is_Associative.html13-Nov-2002 15:43 1.5K 
[TXT]The_Time_Taken_to_do_the_Associativity_of_App_Proof.html13-Nov-2002 15:43 830  
[TXT]The_Tours.html13-Nov-2002 15:43 1.3K 
[TXT]The_WARNING_about_the_Trivial_Consequence.html13-Nov-2002 15:43 1.1K 
[TXT]U.html13-Nov-2002 15:43 796  
[TXT]UBT.html13-Nov-2002 15:43 2.6K 
[TXT]UBT_bang_.html13-Nov-2002 15:43 934  
[TXT]UNARY--.html13-Nov-2002 15:43 827  
[TXT]UNARY-_slash_.html13-Nov-2002 15:43 891  
[TXT]UNCERTIFIED-BOOKS.html13-Nov-2002 15:43 3.6K 
[TXT]UNION-EQ.html13-Nov-2002 15:43 1.1K 
[TXT]UNION-EQUAL.html13-Nov-2002 15:43 1.2K 
[TXT]UNION-THEORIES.html13-Nov-2002 15:43 1.2K 
[TXT]UNIVERSAL-THEORY.html13-Nov-2002 15:43 2.5K 
[TXT]UNMONITOR.html13-Nov-2002 15:43 1.2K 
[TXT]UNSAVE.html13-Nov-2002 15:43 798  
[TXT]UNTRACE$.html13-Nov-2002 15:43 829  
[TXT]UPDATE-NTH.html13-Nov-2002 15:43 1.3K 
[TXT]UPPER-CASE-P.html13-Nov-2002 15:43 834  
[TXT]USING-COMPUTED-HINTS-1.html13-Nov-2002 15:43 1.5K 
[TXT]USING-COMPUTED-HINTS-2.html13-Nov-2002 15:43 4.4K 
[TXT]USING-COMPUTED-HINTS-3.html13-Nov-2002 15:43 5.2K 
[TXT]USING-COMPUTED-HINTS-4.html13-Nov-2002 15:43 6.0K 
[TXT]USING-COMPUTED-HINTS-5.html13-Nov-2002 15:43 2.6K 
[TXT]USING-COMPUTED-HINTS-6.html13-Nov-2002 15:43 10K 
[TXT]USING-COMPUTED-HINTS-7.html13-Nov-2002 15:43 6.8K 
[TXT]USING-COMPUTED-HINTS-8.html13-Nov-2002 15:43 1.7K 
[TXT]USING-COMPUTED-HINTS.html13-Nov-2002 15:43 1.6K 
[TXT]Undocumented_Topic.html13-Nov-2002 15:43 317  
[TXT]Using_the_Associativity_of_App_to_Prove_a_Trivial_Consequence.html13-Nov-2002 15:43 754  
[TXT]VERIFY-GUARDS.html13-Nov-2002 15:43 10K 
[TXT]VERIFY-TERMINATION.html13-Nov-2002 15:43 5.0K 
[TXT]VERIFY.html13-Nov-2002 15:43 1.4K 
[TXT]VERSION.html13-Nov-2002 15:43 4.2K 
[TXT]WELL-FOUNDED-RELATION.html13-Nov-2002 15:43 8.4K 
[TXT]WET.html13-Nov-2002 15:43 3.7K 
[TXT]WHY-BRR.html13-Nov-2002 15:43 3.5K 
[TXT]WITH-ERROR-TRACE.html13-Nov-2002 15:43 473  
[TXT]WITH-LOCAL-STOBJ.html13-Nov-2002 15:43 2.3K 
[TXT]WITH-OUTPUT.html13-Nov-2002 15:43 1.2K 
[TXT]WORLD.html13-Nov-2002 15:43 7.0K 
[TXT]WORMHOLE.html13-Nov-2002 15:43 21K 
[TXT]What_Is_ACL2_lparen_Q_rparen_.html13-Nov-2002 15:43 934  
[TXT]What_is_Required_of_the_User_lparen_Q_rparen_.html13-Nov-2002 15:43 1.0K 
[TXT]What_is_a_Mathematical_Logic_lparen_Q_rparen_.html13-Nov-2002 15:43 1.0K 
[TXT]What_is_a_Mechanical_Theorem_Prover_lparen_Q_rparen_.html13-Nov-2002 15:43 1.0K 
[TXT]What_is_a_Mechanical_Theorem_Prover_lparen_Q_rparen___lparen_continued_rparen_.html13-Nov-2002 15:43 646  
[TXT]XARGS.html13-Nov-2002 15:43 6.5K 
[TXT]You_Must_Think_about_the_Use_of_a_Formula_as_a_Rule.html13-Nov-2002 15:43 1.0K 
[TXT]ZERO-TEST-IDIOMS.html13-Nov-2002 15:43 10K 
[TXT]ZEROP.html13-Nov-2002 15:43 1.2K 
[TXT]ZIP.html13-Nov-2002 15:43 1.4K 
[TXT]ZP.html13-Nov-2002 15:43 1.5K 
[TXT]ZPF.html13-Nov-2002 15:43 730  
[TXT]_at_.html13-Nov-2002 15:43 1.1K 
[TXT]_gt_.html13-Nov-2002 15:43 583  
[TXT]_gt_=.html13-Nov-2002 15:43 603  
[TXT]_hyphen_.html13-Nov-2002 15:43 792  
[TXT]_lt_.html13-Nov-2002 15:43 1.1K 
[TXT]_lt_=.html13-Nov-2002 15:43 600  
[TXT]_slash_.html13-Nov-2002 15:43 892  
[TXT]_slash_=.html13-Nov-2002 15:43 972  
[TXT]_star_.html13-Nov-2002 15:43 741  
[TXT]_star_STANDARD-CI_star_.html13-Nov-2002 15:43 1.0K 
[TXT]_star_STANDARD-CO_star_.html13-Nov-2002 15:43 2.8K 
[TXT]_star_STANDARD-OI_star_.html13-Nov-2002 15:43 963  
[TXT]_star_TERMINAL-MARKUP-TABLE_star_.html13-Nov-2002 15:43 1.8K 
[TXT]acl2-doc-index.html13-Nov-2002 15:43 113K 
[TXT]acl2-doc-major-topics.html13-Nov-2002 15:42 2.4K 
[TXT]acl2-doc.html13-Nov-2002 21:02 9.7K 
[IMG]acl2-system-architecture.gif13-Nov-2002 15:42 8.5K 
[IMG]automatic-theorem-prover.gif13-Nov-2002 15:42 4.4K 
[IMG]binary-trees-app-expl.gif13-Nov-2002 15:42 1.2K 
[IMG]binary-trees-app.gif13-Nov-2002 15:42 1.9K 
[IMG]binary-trees-x-y.gif13-Nov-2002 15:42 1.3K 
[IMG]book04.gif13-Nov-2002 15:42 1.0K 
[IMG]bridge-analysis.gif13-Nov-2002 15:42 2.4K 
[IMG]bridge.gif13-Nov-2002 15:42 4.5K 
[IMG]chem01.gif13-Nov-2002 15:42 1.1K 
[IMG]common-lisp.gif13-Nov-2002 15:42 894  
[IMG]computing-machine-5x7.gif13-Nov-2002 15:42 5.3K 
[IMG]computing-machine-5xy.gif13-Nov-2002 15:42 5.5K 
[IMG]computing-machine-a.gif13-Nov-2002 15:42 6.4K 
[IMG]computing-machine-xxy.gif13-Nov-2002 15:42 6.1K 
[IMG]computing-machine.gif13-Nov-2002 15:42 4.0K 
[IMG]concrete-proof.gif13-Nov-2002 15:42 5.2K 
[IMG]doc03.gif13-Nov-2002 15:42 1.0K 
[IMG]docbag2.gif13-Nov-2002 15:42 1.0K 
[IMG]door02.gif13-Nov-2002 15:42 1.1K 
[IMG]file03.gif13-Nov-2002 15:42 1.0K 
[IMG]file04.gif13-Nov-2002 15:42 1.1K 
[IMG]flying.gif13-Nov-2002 15:42 457  
[IMG]ftp2.gif13-Nov-2002 15:42 1.1K 
[IMG]green-line.gif13-Nov-2002 15:42 114  
[IMG]index.gif13-Nov-2002 15:42 378  
[IMG]info04.gif13-Nov-2002 15:42 1.0K 
[TXT]installation.html13-Nov-2002 20:58 40K 
[IMG]interactive-theorem-prover-a.gif13-Nov-2002 15:42 4.7K 
[IMG]interactive-theorem-prover.gif13-Nov-2002 15:42 5.0K 
[IMG]landing.gif13-Nov-2002 15:42 810  
[IMG]large-flying.gif13-Nov-2002 15:42 1.2K 
[IMG]large-walking.gif13-Nov-2002 15:42 1.3K 
[IMG]llogo.gif13-Nov-2002 15:42 577  
[IMG]logo.gif13-Nov-2002 15:42 3.9K 
[IMG]mailbox1.gif13-Nov-2002 15:42 1.2K 
[TXT]new.html13-Nov-2002 15:42 1.7K 
[IMG]new04.gif13-Nov-2002 15:42 1.1K 
[IMG]note02.gif13-Nov-2002 15:42 1.1K 
[IMG]open-book.gif13-Nov-2002 15:42 2.5K 
[IMG]pisa.gif13-Nov-2002 15:42 1.7K 
[IMG]proof.gif13-Nov-2002 15:42 1.3K 
[IMG]sitting.gif13-Nov-2002 15:42 862  
[IMG]stack.gif13-Nov-2002 15:42 1.8K 
[IMG]state-object.gif13-Nov-2002 15:42 7.3K 
[IMG]teacher1.gif13-Nov-2002 15:42 1.2K 
[IMG]teacher2.gif13-Nov-2002 15:42 1.0K 
[IMG]time-out.gif13-Nov-2002 15:42 1.0K 
[IMG]tools3.gif13-Nov-2002 15:42 1.0K 
[IMG]twarning.gif13-Nov-2002 15:42 71  
[IMG]uaa-rewrite.gif13-Nov-2002 15:42 3.4K 
[IMG]walking.gif13-Nov-2002 15:42 302  
[IMG]warning.gif13-Nov-2002 15:42 215  
[TXT]workshops.html13-Nov-2002 15:42 1.5K 

Apache Server at www.mathcs.duq.edu Port 80