ACL2 Version 1.8

1717 West Sixth Street, Suite 290,
Austin, TX 78703 USA

Matt Kaufmann and J Strother Moore

December 1995

• Index -- alphabetical list of documented topics

• ACL2-TUTORIAL -- tutorial introduction to ACL2

• BDD -- ordered binary decision diagrams with rewriting

• BOOKS -- files of ACL2 event forms

• BREAK-REWRITE -- the read-eval-print loop entered to monitor rewrite rules

• DOCUMENTATION -- functions that display documentation at the terminal

• EVENTS -- functions that extend the logic

• HISTORY -- functions that display or change history

• MISCELLANEOUS -- a miscellany of documented functions and concepts
  (often cited in more accessible documentation)

• OTHER -- other commonly used top-level functions

• PROGRAMMING -- built-in ACL2 functions

• PROOF-CHECKER -- support for low-level interaction

• PROOF-TREE -- proof tree displays

• RELEASE-NOTES -- pointers to what has changed

• RULE-CLASSES -- adding rules to the data base

• THEORIES -- sets of runes to enable/disable in concert