src/HOLCF/Fix.ML
changeset 5143 b94cd208f073
parent 5068 fb28eaa07e01
child 5192 704dd3a6d47d
--- a/src/HOLCF/Fix.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOLCF/Fix.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -884,7 +884,7 @@
         (Simp_tac 1)
         ]);
 
-Goal "!! P. [| adm (%x. P x --> Q x); adm (%x. Q x --> P x) |] \
+Goal "[| adm (%x. P x --> Q x); adm (%x. Q x --> P x) |] \
 \           ==> adm (%x. P x = Q x)";
 by (subgoal_tac "(%x. P x = Q x) = (%x. (P x --> Q x) & (Q x --> P x))" 1);
 by (Asm_simp_tac 1);