UNIVERSAL-THEORY

all rules as of logical name
Major Section:  THEORIES

Examples:
(universal-theory :here)
(universal-theory 'lemma3)
See logical-name.

General Form:
(universal-theory logical-name)
Returns the theory consisting of all the runes that existed immediately after logical-name was introduced. See theories and see logical-name. The theory includes logical-name itself (if there is a rule by that name). (Note that since some events do not introduce rules (e.g., defmacro, defconst or defthm with :rule-classes nil), the universal-theory does not necessarily include a rune for every event name.) The universal-theory is very long and you will probably regret printing it.

You may experience a fencepost problem in deciding which logical-name to use. Deflabel can always be used to mark unambiguously for future reference a particular point in the development of your theory. This is convenient because deflabel does not introduce any rules and hence it doesn't matter if you count it as being in the interval or not. The order of events in the vicinity of an encapsulate is confusing. See encapsulate.

This ``function'' is actually a macro that expands to a term mentioning the single free variable world. When theory expressions are evaluated by in-theory or the :in-theory hint, world is bound to the current ACL2 world.

Also see current-theory. Current-theory is much more commonly used than universal-theory. The former includes only the enabled runes as of the given logical-name, which is probably what you want, while the latter includes disabled ones as well.