next up previous contents
Next: Programming Style Up: Logical Style Previous: Implementation of EFT

The Logical Preamble

The prover automatically loads the declarations of certain logical operators and axioms governing these operators. Most of these are derived from axioms of EFT. They can be examined by starting the prover and looking at the axioms that are present before any theory is loaded.

Randall Holmes
Fri Sep 5 16:28:58 MDT 1997