changeset 4642 | 2d3910d6ab10 |
parent 4477 | b3e5857d8d99 |
child 4833 | 2e53109d4bc8 |
--- a/src/HOLCF/Tr.ML Fri Feb 20 17:56:51 1998 +0100 +++ b/src/HOLCF/Tr.ML Fri Feb 20 17:57:16 1998 +0100 @@ -134,7 +134,6 @@ goal thy "(Def x = FF) = (~x)"; by (simp_tac (simpset() addsimps [FF_def]) 1); -by (fast_tac HOL_cs 1); qed"Def_bool2"; goal thy "(Def x = TT) = x"; @@ -187,4 +186,4 @@ by (REPEAT ((resolve_tac (adm_lemmas@cont_lemmas1) 1) ORELSE atac 1)); qed"adm_nFF"; -Addsimps [adm_nTT,adm_nFF]; \ No newline at end of file +Addsimps [adm_nTT,adm_nFF];