• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
    • Break-rewrite
    • Proof-builder
    • Accumulated-persistence
    • Cgen
    • Proof-tree
      • Proof-tree-examples
      • Proof-tree-details
      • Stop-proof-tree
      • Start-proof-tree
      • Checkpoint-forced-goals
    • Forward-chaining-reports
    • Print-gv
    • Dmr
    • Splitter
    • Guard-debug
    • Set-debugger-enable
    • Redo-flat
    • Set-check-invariant-risk
    • Time-tracker
    • Removable-runes
    • Efficiency
    • Tail-biting
    • Failed-forcing
    • Sneaky
    • Invariant-risk
    • Failure
    • Measure-debug
    • Dead-events
    • Remove-hyps
    • Type-prescription-debugging
    • Pstack
    • Set-register-invariant-risk
    • Trace
    • 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
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Proof-tree

Stop-proof-tree

Stop displaying proof trees during proofs

Also see proof-tree and see start-proof-tree. Note that :stop-proof-tree works by adding 'proof-tree to the inhibit-output-lst; see set-inhibit-output-lst.

Proof tree displays are explained in the documentation for proof-tree. :Stop-proof-tree causes proof tree display to be turned off.

It is permissible to submit the form (stop-proof-tree) during a break. Thus, you can actually turn off proof tree display in the middle of a proof by interrupting ACL2 and submitting the form (stop-proof-tree) in raw Lisp.