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

• ACL2-HELP -- the acl2-help mailing list

• 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

• 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

• PSO -- show the most recently saved output

• PSO! -- show the most recently saved output, including proof-tree output

• 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

• SAVE-EXEC -- save an executable image and (for most Common Lisps) a wrapper script

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

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

• SET-PRINT-CLAUSE-IDS -- cause subgoal numbers to be printed when 'prove output is inhibited

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

• SET-SAVED-OUTPUT -- save proof output for later display with :pso or :pso!

• SET-TAINTED-OKP -- control output

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

• THM -- prove a theorem

• TIME$ -- time a form

• TRANS -- print the macroexpansion of a form

• TRANS! -- print the macroexpansion of a form without single-threadedness concerns

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