		Search-engine friendly clone of the ACL2 documentation.

Minimal-theory

A minimal theory to enable

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.