Major Section: THEORIES
Example: (enable fact (fact) associativity-of-app)where each
General Form: (enable name1 name2 ... namek)
nameiis a runic designator; see theories. The result is the theory that contains all the names in the current theory plus those listed. Note that this is merely a function that returns a theory. The result is generally a very long list of runes and you will probably regret printing it.
The standard way to ``enable'' a fixed set of names, is
(in-theory (enable name1 name2 ... namek)) ; globally :in-theory (enable name1 name2 ... namek) ; locallyNote that all the names are implicitly quoted. If you wish to enable a computed list of names,
lst, use the theory expression
(union-theories (current-theory :here) lst).