• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • 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
        • 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
        • Recursion-and-induction
        • Hons-and-memoization
        • Events
        • Parallelism
        • History
        • Programming
        • Operational-semantics
        • Real
        • Start-here
        • Debugging
        • Miscellaneous
        • Output-controls
        • Macros
        • Interfacing-tools
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Theories
    • Theory-functions

    Ground-zero

    enabled rules in the startup theory

    ACL2 concludes its initialization (boot-strapping) procedure by defining the theory ground-zero; see theories. In fact, this theory is just the theory defined by (current-theory :here) at the conclusion of initialization; see current-theory.

    Note that by evaluating the event

    (in-theory (current-theory 'ground-zero))

    you can restore the current theory to its value at the time you started up ACL2.