All rules as of logical name
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
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
Also see current-theory.