• 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
          • Disable
          • Enable
          • Current-theory
          • Syntactically-clean-lambda-objects-theory
          • Hands-off-lambda-objects-theory
          • Rewrite-lambda-objects-theory
          • Theory
          • Universal-theory
          • E/d
          • Executable-counterpart-theory
          • Function-theory
          • Set-difference-theories
          • Minimal-theory
          • Ground-zero
            • Union-theories
            • Intersection-theories
          • 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.