Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Break-rewrite
Proof-builder
Instructions
Proof-builder-commands
ACL2-pc::rewrite
ACL2-pc::apply-linear
ACL2-pc::sequence
Proof-builder-commands-short-list
ACL2-pc::=
ACL2-pc::s
ACL2-pc::exit
ACL2-pc::type-alist
ACL2-pc::in-theory
ACL2-pc::equiv
ACL2-pc::comm
ACL2-pc::casesplit
ACL2-pc::add-abbreviation
ACL2-pc::dv
ACL2-pc::hyps
ACL2-pc::prove-termination
ACL2-pc::prove-guard
ACL2-pc::x
ACL2-pc::pot-lst
ACL2-pc::fancy-use
ACL2-pc::dive
ACL2-pc::generalize
ACL2-pc::lisp
ACL2-pc::show-rewrites
ACL2-pc::claim
ACL2-pc::put
ACL2-pc::split
ACL2-pc::geneqv
ACL2-pc::prove
ACL2-pc::help
ACL2-pc::save
ACL2-pc::do-all
ACL2-pc::demote
ACL2-pc::wrap1
ACL2-pc::show-abbreviations
ACL2-pc::promote
ACL2-pc::retrieve
ACL2-pc::reduce
ACL2-pc::forwardchain
ACL2-pc::doc
ACL2-pc::bash
ACL2-pc::p-top
ACL2-pc::print
ACL2-pc::expand
ACL2-pc::bk
ACL2-pc::wrap
ACL2-pc::remove-abbreviations
ACL2-pc::reduce-by-induction
ACL2-pc::induct
ACL2-pc::unsave
ACL2-pc::undo
ACL2-pc::top
ACL2-pc::restore
ACL2-pc::replay
ACL2-pc::psog
ACL2-pc::p
ACL2-pc::nx
ACL2-pc::noise
ACL2-pc::contrapose
ACL2-pc::wrap-induct
ACL2-pc::pso!
ACL2-pc::pso
ACL2-pc::up
ACL2-pc::then
ACL2-pc::th
ACL2-pc::sl
ACL2-pc::show-type-prescriptions
ACL2-pc::bdd
ACL2-pc::repeat
ACL2-pc::pr
ACL2-pc::pl
ACL2-pc::finish
ACL2-pc::commands
ACL2-pc::change-goal
ACL2-pc::use
ACL2-pc::show-linears
ACL2-pc::s-prop
ACL2-pc::runes
ACL2-pc::protect
ACL2-pc::instantiate
ACL2-pc::insist-all-proved
ACL2-pc::fail
ACL2-pc::clause-processor
ACL2-pc::bookmark
ACL2-pc::retain
ACL2-pc::quiet!
ACL2-pc::pro
ACL2-pc::orelse
ACL2-pc::goals
ACL2-pc::drop
ACL2-pc::do-strict
ACL2-pc::print-all-concs
ACL2-pc::do-all-no-prompt
ACL2-pc::x-dumb
ACL2-pc::succeed
ACL2-pc::print-all-goals
ACL2-pc::pp
ACL2-pc::noise!
ACL2-pc::nil
ACL2-pc::negate
ACL2-pc::illegal
ACL2-pc::elim
ACL2-pc::sls
ACL2-pc::quiet
ACL2-pc::claim-simple
ACL2-pc::cg
ACL2-pc::pro-or-skip
ACL2-pc::ex
ACL2-pc::comment
ACL2-pc::ACL2-wrap
ACL2-pc::when-not-proved
ACL2-pc::skip
ACL2-pc::retain-or-skip
ACL2-pc::repeat-until-done
ACL2-pc::free
ACL2-pc::drop-or-skip
ACL2-pc::cg-or-skip
ACL2-pc::by
ACL2-pc::split-in-theory
ACL2-pc::st
ACL2-pc::sr
ACL2-pc::print-main
ACL2-pc::lemmas-used
ACL2-pc::cl-proc
ACL2-pc::al
ACL2-pc::run-instr-on-new-goals
ACL2-pc::run-instr-on-goal
ACL2-pc::repeat-rec
ACL2-pc::r
ACL2-pc::contradict
Proof-builder-commands-short-list
Dive-into-macros-table
Verify
Define-pc-macro
Macro-command
Define-pc-help
Toggle-pc-macro
Define-pc-meta
Retrieve
Unsave
Proof-checker
Accumulated-persistence
Cgen
Forward-chaining-reports
Proof-tree
Print-gv
Dmr
With-brr-data
Splitter
Set-debugger-enable
Guard-debug
Redo-flat
Time-tracker
Set-check-invariant-risk
Removable-runes
Efficiency
Explain-near-miss
Tail-biting
Failed-forcing
Sneaky
Invariant-risk
Failure
Measure-debug
Dead-events
Compare-objects
Remove-hyps
Type-prescription-debugging
Pstack
Trace
Set-register-invariant-risk
Walkabout
Disassemble$
Nil-goal
Cw-gstack
Set-guard-msg
Find-lemmas
Watch
Quick-and-dirty-subsumption-replacement-step
Profile-all
Profile-ACL2
Set-print-gv-defaults
Minimal-runes
Spacewalk
Try-gl-concls
Near-misses
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Proof-builder-commands
ACL2-pc::cl-proc
(macro) same as
clause-processor
This is simply an abbreviation for
ACL2-pc::clause-processor
.