| author | oheimb |
| Mon, 12 Apr 2004 12:52:08 +0200 | |
| changeset 14536 | 43e436a4f293 |
| 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"; |