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.
