Documentation for ACL2 Version 3.6.1
The ACL2 Documentation is divided into the following Major TopicsACL2-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
EVENTS -- functions that extend the logic
HISTORY -- functions that display or change history
HONS-AND-MEMOIZATION -- hash cons, function memoization, and applicative hash tables
IO -- input/output facilities in ACL2
MISCELLANEOUS -- a miscellany of documented functions and concepts
(often cited in more accessible documentation)
OTHER -- other commonly used top-level functions
PARALLELISM -- experimental extension for evaluating forms in parallel
PROGRAMMING -- built-in ACL2 functions
PROOF-CHECKER -- support for low-level interaction
PROOF-TREE -- proof tree displays
-
REAL -- ACL2(r) support for real numbers
RELEASE-NOTES -- pointers to what has changed
RULE-CLASSES -- adding rules to the data base
STOBJ -- single-threaded objects or ``von Neumann bottlenecks''
-
THEORIES -- sets of runes to enable/disable in concert
TRACE -- tracing functions in ACL2