• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
      • Rune
      • In-theory
      • Disable
      • Enable
      • Theories-and-primitives
      • Deftheory
      • Theory-functions
      • Deftheory-static
      • Current-theory
      • Syntactically-clean-lambda-objects-theory
      • Hands-off-lambda-objects-theory
      • Rewrite-lambda-objects-theory
      • Rulesets
        • Expand-ruleset
        • E/d*
        • Ruleset
        • Def-ruleset
        • Get-ruleset
        • Disable*
        • Def-ruleset!
        • Enable*
        • Add-to-ruleset
      • Theory
      • Disabledp
      • Universal-theory
      • Using-enabled-rules
      • E/d
      • Active-runep
      • Executable-counterpart-theory
      • Function-theory
      • Set-difference-theories
      • Minimal-theory
      • Ground-zero
      • Union-theories
      • Intersection-theories
      • Incompatible
      • Defthy
      • Incompatible!
      • Active-or-non-runep
      • Rule-names
    • Rule-classes
    • Proof-builder
    • Hons-and-memoization
    • Events
    • History
    • Parallelism
    • Programming
    • Start-here
    • Real
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Rulesets

Disable*

Ruleset-aware version of disable.

Examples:

(in-theory (disable* my-rules append car-cons))

(defthm ...
   :hints (("Goal" :in-theory (disable* foo ...))))