--- a/src/HOLCF/Lift3.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOLCF/Lift3.ML Wed Jul 15 10:15:13 1998 +0200
@@ -139,13 +139,13 @@
(* Two specific lemmas for the combination of LCF and HOL terms *)
-Goal "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s)";
+Goal "[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s)";
by (rtac cont2cont_CF1L 1);
by (REPEAT (resolve_tac cont_lemmas1 1));
by Auto_tac;
qed"cont_fapp_app";
-Goal "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s t)";
+Goal "[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s t)";
by (rtac cont2cont_CF1L 1);
by (etac cont_fapp_app 1);
by (assume_tac 1);