Documentation for ACL2 Version 6.0
The ACL2 Documentation is divided into the following Major Topics

ACL2TUTORIAL  tutorial introduction to ACL2
BDD  ordered binary decision diagrams with rewriting
BOOKS  files of ACL2 event forms
BREAKREWRITE  the readevalprint loop entered to monitor rewrite rules
DOCUMENTATION  functions that display documentation
EVENTS  functions that extend the logic
FORWARDCHAININGREPORTS  to see reports about the forward chaining process
HISTORY  functions that display or change history
HONSANDMEMOIZATION  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 toplevel functions
PARALLELISM  experimental extension for parallel execution and proofs
PROGRAMMING  programming in ACL2
PROOFCHECKER  support for lowlevel interaction
PROOFTREE  proof tree displays

REAL  ACL2(r) support for real numbers
RELEASENOTES  pointers to what has changed
RULECLASSES  adding rules to the database
SERIALIZE  routines for saving ACL2 objects to files, and later restoring them
STOBJ  singlethreaded objects or ``von Neumann bottlenecks''


TRACE  tracing functions in ACL2