Ihs-theories
Subtheories of the ACL2 initialization theory.
Note: Jared recommends against following the advice below. In
particular, using (in-theory nil) is probably not a good idea most of the
time.
The conventional way to initiate the definition of a book in the IHS library
hierarchy is to
- Include all necessary books
- DISABLE the world with (IN-THEORY NIL), and
- Construct the theory needed to certify
the present book from theory expressions supplied by the included books.
The ihs-theories book includes the most basic theories, i.e., theories
of the ACL2 functions available at this label: 'IHS-THEORIES, which is exactly
the extension of the ACL2 initialization theory made by "ihs-init". Every
IHS book will normally begin by ENABLEing one of these theories. Some of the
theories may also be useful, for example, to specify very restricted local
theories for specialized apllications.
Subtopics
- Basic-boot-strap
- A controlled boot-strap theory.
- Measures
- Functions used to prove admissibility.
- Built-ins
- Functions whose definitions are "built in" to ACL2.
