--- a/src/HOLCF/Lift2.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Lift2.ML Fri Oct 10 19:02:28 1997 +0200
@@ -9,7 +9,7 @@
open Lift2;
(* for compatibility with old HOLCF-Version *)
-qed_goal "inst_lift_po" thy "(op <<)=(%x y.x=y|x=Undef)"
+qed_goal "inst_lift_po" thy "(op <<)=(%x y. x=y|x=Undef)"
(fn prems =>
[
(fold_goals_tac [less_lift_def]),
@@ -26,7 +26,7 @@
bind_thm ("UU_lift_def",minimal_lift RS minimal2UU RS sym);
-qed_goal "least_lift" thy "? x::'a lift.!y.x<<y"
+qed_goal "least_lift" thy "? x::'a lift.!y. x<<y"
(fn prems =>
[
(res_inst_tac [("x","Undef")] exI 1),
@@ -57,7 +57,7 @@
goal Lift2.thy
"!!Y. [|? j.~Y(j)=Undef;is_chain(Y::nat=>('a)lift)|] \
-\ ==> ? j.!i.j<i-->~Y(i)=Undef";
+\ ==> ? j.!i. j<i-->~Y(i)=Undef";
by Safe_tac;
by (Step_tac 1);
by (strip_tac 1);
@@ -74,7 +74,7 @@
"(! Y. is_chain(Y::nat=>('a)lift)-->(? n. max_in_chain n Y))";
by (rewtac max_in_chain_def);
by (strip_tac 1);
-by (res_inst_tac [("P","!i.Y(i)=Undef")] case_split_thm 1);
+by (res_inst_tac [("P","!i. Y(i)=Undef")] case_split_thm 1);
by (res_inst_tac [("x","0")] exI 1);
by (strip_tac 1);
by (rtac trans 1);
@@ -82,7 +82,7 @@
by (rtac sym 1);
by (etac spec 1);
-by (subgoal_tac "!x y.x<<(y::('a)lift) --> x=Undef | x=y" 1);
+by (subgoal_tac "!x y. x<<(y::('a)lift) --> x=Undef | x=y" 1);
by (simp_tac (!simpset addsimps [inst_lift_po]) 2);
by (rtac (chain_mono2_po RS exE) 1);
by (Fast_tac 1);
@@ -110,7 +110,7 @@
(* Main Lemma: cpo_lift *)
goal Lift2.thy
- "!!Y. is_chain(Y::nat=>('a)lift) ==> ? x.range(Y) <<|x";
+ "!!Y. is_chain(Y::nat=>('a)lift) ==> ? x. range(Y) <<|x";
by (cut_inst_tac [] flat_imp_chain_finite_poo 1);
by (Step_tac 1);
by Safe_tac;