OTHER

Major Section:  ACL2 Documentation

• @ -- get the value of a global variable in state

• ACL2-DEFAULTS-TABLE -- a table specifying certain defaults, e.g., the default defun-mode

• ASSIGN -- assign to a global variable in state

• CERTIFY-BOOK -- how to produce a certificate for a book

• CERTIFY-BOOK! -- a variant of certify-book

• COMP -- compile some ACL2 functions

• CW-GSTACK -- debug a rewriting loop or stack overflow

• EXIT -- quit entirely out of Lisp

• GOOD-BYE -- quit entirely out of Lisp

• LD -- the ACL2 read-eval-print loop, file loader, and command processor

• PROPS -- print the ACL2 properties on a symbol

• PSTACK -- seeing what is the prover up to

• Q -- quit ACL2 (type :q) -- reenter with (lp)

• QUIT -- quit entirely out of Lisp

• REBUILD -- a convenient way to reconstruct your old state

• RESET-LD-SPECIALS -- restores initial settings of the ld specials

• SET-GUARD-CHECKING -- control checking guards during execution of top-level forms

• SET-INHIBIT-OUTPUT-LST -- control output

• SET-RAW-MODE -- enter or exit ``raw mode,'' a raw Lisp environment

• SKIP-PROOFS -- skip proofs for a given form -- a quick way to introduce unsoundness

• THM -- prove a theorem

• TRANS -- print the macroexpansion of a form

• TRANS1 -- print the one-step macroexpansion of a form