• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
      • Std/lists
      • Std/alists
      • Obags
      • Std/util
        • Defprojection
        • Deflist
        • Defaggregate
        • Define
        • Defmapping
        • Defenum
        • Add-io-pairs
        • Defalist
        • Defmapappend
        • Returns-specifiers
        • Defarbrec
        • Define-sk
        • Defines
        • Error-value-tuples
        • Defmax-nat
        • Defmin-int
        • Deftutorial
        • Extended-formals
        • Defrule
          • Rule
          • Defruledl
            • Defruled
            • Defrulel
          • Defval
          • Defsurj
          • Defiso
          • Defconstrained-recognizer
          • Deffixer
          • Defmvtypes
          • Defconsts
          • Defthm-unsigned-byte-p
          • Support
          • Defthm-signed-byte-p
          • Defthm-natp
          • Defund-sk
          • Defmacro+
          • Defsum
          • Defthm-commutative
          • Definj
          • Defirrelevant
          • Defredundant
        • Std/strings
        • Std/osets
        • Std/io
        • Std/basic
        • Std/system
        • Std/typed-lists
        • Std/bitsets
        • Std/testing
        • Std/typed-alists
        • Std/stobjs
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Defrule

    Defruledl

    Variant of defrule that disables the theorem afterwards and makes it local.

    This is identical to defrule except that the theorem is generated using defthmd instead of defthm and the :local argument is set to t.