| | | A.3.3 Formula Declarations |
I: FORMULA E
I: AXIOM E
This declaration introduces a formula constant I with value E of type BOOLEAN; the formula denoted by I is consequently assumed to be true.
If the declaration is tagged with the keyword FORMULA, the formula needs proof; it can be also used as an additional assumption in the proof of another formula by use of the lemma command.
If the declaration is tagged with the keyword AXIOM, the formula does not need proof; it is automatically imported as an additional assumption into the proof of every subsequent formula.
Type checking E may give rise to a type checking condition.
| | | A.3.3 Formula Declarations |