# HG changeset patch
# User nipkow
# Date 887993836 -3600
# Node ID 2d3910d6ab10233d4243f4588c675b9a1ec908aa
# Parent  70a50c2a920fb149c8ff7378a53cd8fd1cb5ebec
*** empty log message ***

diff -r 70a50c2a920f -r 2d3910d6ab10 src/HOLCF/Tr.ML
--- 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];