GROUND-ZERO

enabled rules in the startup theory
Major Section:  THEORIES

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.