• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
    • 100-theorems
    • Arithmetic
    • Bit-vectors
      • Sparseint
      • Bitops
      • Bv
      • Ihs
        • Logops-definitions
        • Math-lemmas
        • Ihs-theories
        • Ihs-init
          • Ihs-utilities
            • Defun-type/exec-theory
            • Defun-theory
            • Definition-free-theory
            • Rewrite-theory
            • Rewrite-free-theory
            • Definition-theory
            • Mlambda
            • Enable-theory
            • Disable-theory
        • Logops
      • Rtl
    • Algebra
  • Testing-utilities

• Ihs-utilities

Disable-theory

Creates an IN-THEORY event that is equivalent to DISABLEing the theory-expression. Note that theory-expression is evaluated.