Major Section: THEORIES
This theory (see theories) enables only a few built-in functions and
executable counterparts. It can be useful when you want to formulate lemmas
that rather immediately imply the theorem to be proved, by way of a :use
hint (see hints), for example as follows.
:use (lemma-1 lemma-2 lemma-3) :in-theory (union-theories '(f1 f2) (theory 'minimal-theory))In this example, we expect the current goal to follow from lemmas
lemma-1, lemma-2, and lemma-3 together with rules f1 and
f2 and some obvious facts about built-in functions (such as the
definition of implies and the :executable-counterpart of
car). The :in-theory hint above is intended to speed up the
proof by turning off all inessential rules.
