| author | wenzelm |
| Sat, 15 Apr 2000 15:00:57 +0200 | |
| changeset 8717 | 20c42415c07d |
| 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"; |