• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
      • Gentle-introduction-to-ACL2-programming
      • ACL2-tutorial
      • About-ACL2
        • Recursion-and-induction
        • Operational-semantics
        • Soundness
        • Release-notes
          • Note-2-8
          • Note-2-7
            • Note-2-7-bug-fixes
            • Note-2-7-new-functionality
            • Note-2-7-proofs
            • Note-2-7-other
            • Note-2-7-system
            • Note-2-7-rules
            • Note-2-7-guards
            • Note-2-7-proof-builder
          • Note-8-6
          • Note-8-2
          • Note-7-0
          • Note-8-5
          • Note-8-3
          • Note-8-1
          • Note-8-0
          • Note-7-1
          • Note-6-4
          • Note-2-9-3
          • Note-2-9-1
          • Note-8-4
          • Note-7-2
          • Note-6-5
          • Note-4-0
          • Note-2-9-2
          • Note-3-6
          • Note-3-3
          • Note-3-2-1
          • Note-3-0-1
          • Note-2-9-5
          • Note-2-5
          • Note-1-5
          • Note-6-1
          • Note-4-3
          • Note-4-2
          • Note-4-1
          • Note-3-5
          • Note-3-4
          • Note-3-2
          • Note-3-0-2
          • Note-2-9-4
          • Note-2-9
          • Note-1-8
          • Note-1-7
          • Note-1-6
          • Note-1-4
          • Note-1-3
          • Note-7-4
          • Note-7-3
          • Note-6-3
          • Note-6-2
          • Note-6-0
          • Note-5-0
          • Note-8-7
          • Note-1-9
          • Note-2-2
          • Note-1-8-update
          • Note-3-5(r)
          • Note-2-3
          • Release-notes-books
          • Note-3-6-1
          • Note-1-2
          • Note-2-4
          • Note-2-6
          • Note-2-0
          • Note-3-0
          • Note-3-2(r)
          • Note-2-7(r)
          • Note-1-1
          • Note-3-4(r)
          • Note-3-1
          • Note-2-8(r)
          • Note-2-1
          • Note-2-9(r)
          • Note-2-6(r)
          • Note-3-1(r)
          • Note-3-0(r)
          • Note-3-0-1(r)
          • Note-2-5(r)
          • Note-4-3(r)
          • Note-4-2(r)
          • Note-4-1(r)
          • Note-4-0(r)
          • Note-3-6(r)
          • Note-3-3(r)
          • Note-3-2-1(r)
        • Version
        • Acknowledgments
        • Pre-built-binary-distributions
        • Common-lisp
        • Git-quick-start
        • Copyright
        • Building-ACL2
        • ACL2-help
        • Bibliography
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Note-2-7

Note-2-7-proof-builder

ACL2 Version 2.7 Notes on proof-builder Changes

Output from the proof-builder can now be inhibited by supplying the symbol proof-builder in the list given to set-inhibit-output-lst.