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.
