Major Section: THEORIES
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
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-3together with rules
f2and some obvious facts about built-in functions (such as the definition of
in-theoryhint above is intended to speed up the proof by turning off all inessential rules.