• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • 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
          • Basic-boot-strap
          • Measures
          • Built-ins
            • Builtin-defaxioms/defthms
              • Builtin-defthms
              • Builtin-defaxioms
              • Builtin-defaxioms/defthms-by-rule-classes
              • Builtin-defaxioms/defthms-by-types/functions
        • Ihs-init
        • Logops
      • Rtl
    • Algebra
  • Testing-utilities

• Built-ins

Builtin-defaxioms/defthms

Built-in axioms and theorems.

Subtopics

Builtin-defthms

All built-in theorems.

Builtin-defaxioms

All built-in axioms.

Builtin-defaxioms/defthms-by-rule-classes

Built-in axioms and theorems, organized by rule-classes.

Builtin-defaxioms/defthms-by-types/functions

Built-in axioms and theorems, organized by types and functions.