Perhaps the most commonly used proof-builder commands

The list of subtopics below includes what are arguably the most useful, and most commonly used, proof-builder commands.

- ACL2-pc::=
- (atomic macro) attempt an equality (or equivalence) substitution
- ACL2-pc::s
- (primitive) simplify the current subterm
- ACL2-pc::exit
- (meta) exit the interactive proof-builder
- ACL2-pc::in-theory
- (primitive) set the current proof-builder theory
- ACL2-pc::comm
- (macro) display instructions from the current interactive session
- ACL2-pc::dv
- (atomic macro) move to the indicated subterm
- ACL2-pc::x
- (atomic macro) expand and (maybe) simplify function call at the current subterm
- ACL2-pc::show-rewrites
- (macro) display the applicable rewrite rules
- ACL2-pc::claim
- (atomic macro) add a new hypothesis
- ACL2-pc::split
- (atomic macro) split the current goal into cases
- ACL2-pc::prove
- (primitive) call the ACL2 theorem prover to prove the current goal
- ACL2-pc::save
- (macro) save the proof-builder state (state-stack)
- ACL2-pc::demote
- (primitive) move top-level hypotheses to the conclusion
- ACL2-pc::retrieve
- (macro) re-enter the proof-builder
- ACL2-pc::p-top
- (macro) prettyprint the conclusion, highlighting the current term
- ACL2-pc::bash
- (atomic macro) call the ACL2 theorem prover's simplifier
- ACL2-pc::expand
- (primitive) expand the current function call without simplification
- ACL2-pc::bk
- (atomic macro) move backward one argument in the enclosing term
- ACL2-pc::induct
- (atomic macro) generate subgoals using induction
- ACL2-pc::undo
- (meta) undo some instructions
- ACL2-pc::top
- (atomic macro) move to the top of the goal
- ACL2-pc::restore
- (meta) remove the effect of an UNDO command
- ACL2-pc::replay
- (macro) replay one or more instructions
- ACL2-pc::p
- (macro) prettyprint the current term in the usual user-level (untranslated) syntax
- ACL2-pc::nx
- (atomic macro) move forward one argument in the enclosing term
- ACL2-pc::contrapose
- (primitive) switch a hypothesis with the conclusion, negating both
- ACL2-pc::up
- (primitive) move to the parent (or some ancestor) of the current subterm
- ACL2-pc::th
- (macro) print the top-level hypotheses and the current subterm
- ACL2-pc::use
- (atomic macro) use a lemma instance
- ACL2-pc::s-prop
- (atomic macro) simplify propositionally
- ACL2-pc::runes
- (macro) print the runes (definitions, lemmas, ...) used
- ACL2-pc::goals
- (macro) list the names of goals on the stack
- ACL2-pc::drop
- (primitive) drop top-level hypotheses
- ACL2-pc::x-dumb
- (atomic macro) expand function call at the current subterm, without simplifying
- ACL2-pc::cg
- (macro) change to another goal.
- ACL2-pc::sr
- (macro) same as SHOW-REWRITES
- ACL2-pc::r
- (macro) same as rewrite