## 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.