--- a/src/HOLCF/Lift3.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Lift3.ML Fri Oct 10 19:02:28 1997 +0200
@@ -80,7 +80,7 @@
section"UU and Def";
(* ---------------------------------------------------------- *)
-goal thy "x=UU | (? y.x=Def y)";
+goal thy "x=UU | (? y. x=Def y)";
by (lift.induct_tac "x" 1);
by (Asm_simp_tac 1);
by (rtac disjI2 1);
@@ -100,7 +100,7 @@
by (ALLGOALS Asm_simp_tac);
qed "expand_lift_case";
-goal thy "(x~=UU)=(? y.x=Def y)";
+goal thy "(x~=UU)=(? y. x=Def y)";
by (rtac iffI 1);
by (rtac Lift_cases 1);
by (REPEAT (fast_tac (HOL_cs addSIs lift.distinct) 1));