		Search-engine friendly clone of the ACL2 documentation.

ACL2

ACL2 system documentation

Those topics that pertain to the ACL2 system belong under this node of the documentation. See top for the top node of this manual, under which may be found many topics pertaining to the community-books.

Subtopics

Theories: Sets of runes to enable/disable in concert
Rule-classes: Adding rules to the database
Proof-builder: An interactive tool for controlling ACL2's proof processes.
Recursion-and-induction: Recursion and Induction
Hons-and-memoization: Hash cons, function memoization, and applicative hash tables
Events: Functions that extend the logic
Parallelism: Experimental extension for parallel execution and proofs
History: Functions to display or change contents of the logical world
Programming: Programming in ACL2
Operational-semantics: Modeling State Machines
Real: ACL2(r) support for real numbers
Start-here: Introductory information about ACL2
Miscellaneous: A miscellany of documented functions and concepts (often cited in more accessible documentation)
Output-controls: Methods for controlling the output produced by the ACL2 prover
Bdd: Ordered binary decision diagrams with rewriting
Macros: Macros allow you to extend the syntax of ACL2.
Installation: Installation Guide
Mailing-lists: Mailing lists for ACL2 users