author | wenzelm |
Sat, 01 Jul 2000 19:49:20 +0200 | |
changeset 9226 | cbe6144f0f15 |
parent 5377 | efb799c5ed3c |
permissions | -rw-r--r-- |
use "bool2if.ML"; use "proof.ML"; qed "bool2if_correct"; use "normif.ML"; use "proof.ML"; qed_spec_mp "normif_correct"; Addsimps [normif_correct]; use "norm.ML"; use "proof.ML"; qed "norm_correct"; use "normal_normif.ML"; use "proof.ML"; qed_spec_mp "normal_normif"; Addsimps [normal_normif]; use "normal_norm.ML"; use "proof.ML"; qed "normal_norm";