--- a/src/HOLCF/Lift.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Lift.ML Fri Oct 10 19:02:28 1997 +0200
@@ -22,7 +22,7 @@
(* flift1 is continuous in a variable that occurs only
in the Def branch *)
-goal thy "!!f. [| !! a.cont (%y. (f y) a) |] ==> \
+goal thy "!!f. [| !! a. cont (%y. (f y) a) |] ==> \
\ cont (%y. lift_case UU (f y))";
by (rtac cont2cont_CF1L_rev 1);
by (strip_tac 1);
@@ -34,7 +34,7 @@
(* flift1 is continuous in a variable that occurs either
in the Def branch or in the argument *)
-goal thy "!!f. [| !! a.cont (%y. (f y) a); cont g|] ==> \
+goal thy "!!f. [| !! a. cont (%y. (f y) a); cont g|] ==> \
\ cont (%y. lift_case UU (f y) (g y))";
by (rtac cont2cont_app 1);
back();