## MINIMAL-THEORY

a minimal theory to enable
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.