| author | wenzelm |
| Mon, 28 Jan 2002 18:51:48 +0100 | |
| changeset 12858 | 6214f03d6d27 |
| parent 5377 | efb799c5ed3c |
| permissions | -rw-r--r-- |
| 5377 | 1 |
use "normif.ML"; |
2 |
use "proof.ML"; |
|
3 |
qed_spec_mp "normif_correct"; |
|
4 |
Addsimps [normif_correct]; |
|
5 |
||
6 |
use "norm.ML"; |
|
7 |
use "proof.ML"; |
|
8 |
qed "norm_correct"; |
|
9 |
||
10 |
Goal "!t e. normal t & normal e --> normal(normif b t e)"; |
|
11 |
use "proof.ML"; |
|
12 |
qed_spec_mp "normal_normif"; |
|
13 |
Addsimps [normal_normif]; |
|
14 |
||
15 |
use "normal_norm.ML"; |
|
16 |
use "proof.ML"; |
|
17 |
qed "normal_norm"; |