author | wenzelm |
Fri, 16 Jul 1999 22:24:42 +0200 | |
changeset 7024 | 44bd3c094fd6 |
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"; |