| author | wenzelm |
| Wed, 25 Aug 1999 20:49:02 +0200 | |
| changeset 7357 | d0e16da40ea2 |
| parent 5377 | efb799c5ed3c |
| permissions | -rw-r--r-- |
| 5377 | 1 |
use "bool2if.ML"; |
2 |
use "proof.ML"; |
|
3 |
qed "bool2if_correct"; |
|
4 |
||
5 |
use "normif.ML"; |
|
6 |
use "proof.ML"; |
|
7 |
qed_spec_mp "normif_correct"; |
|
8 |
Addsimps [normif_correct]; |
|
9 |
||
10 |
use "norm.ML"; |
|
11 |
use "proof.ML"; |
|
12 |
qed "norm_correct"; |
|
13 |
||
14 |
use "normal_normif.ML"; |
|
15 |
use "proof.ML"; |
|
16 |
qed_spec_mp "normal_normif"; |
|
17 |
Addsimps [normal_normif]; |
|
18 |
||
19 |
use "normal_norm.ML"; |
|
20 |
use "proof.ML"; |
|
21 |
qed "normal_norm"; |