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-namewas introduced. See theories and see logical-name. The theory includes
logical-nameitself (if there is a rule by that name). (Note that since some events do not introduce rules (e.g.,
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
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
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.