| | | B.4.8 lemma: Import Lemmas |
lemma L1, L2, ...
In proving mode.
This command adds the formulas with labels L1, L2, ... as assumptions to the current proof state. These formulas must be defined in declaration mode before the formula that is currently proved. This implements the following rule:
[E] |- L1: FORMULA = F1
[E] |- L2: FORMULA = F2
...
[E] ..., F1, F2 |- ...
-------------------------------
[E] ... |- ....
By the application of this command, the status of the current proof also depends on the proof status of these formulas; in particular, the current proof is only considered complete, if also these formulas have complete proofs.
| | | B.4.8 lemma: Import Lemmas |