--- a/src/HOLCF/Up2.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Up2.ML Fri Oct 10 19:02:28 1997 +0200
@@ -9,7 +9,7 @@
open Up2;
(* for compatibility with old HOLCF-Version *)
-qed_goal "inst_up_po" thy "(op <<)=(%x1 x2.case Rep_Up(x1) of \
+qed_goal "inst_up_po" thy "(op <<)=(%x1 x2. case Rep_Up(x1) of \
\ Inl(y1) => True \
\ | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False \
\ | Inr(z2) => y2<<z2))"
@@ -31,7 +31,7 @@
bind_thm ("UU_up_def",minimal_up RS minimal2UU RS sym);
-qed_goal "least_up" thy "? x::'a u.!y.x<<y"
+qed_goal "least_up" thy "? x::'a u.!y. x<<y"
(fn prems =>
[
(res_inst_tac [("x","Abs_Up(Inl ())")] exI 1),
@@ -99,7 +99,7 @@
(* Some kind of surjectivity lemma *)
(* ------------------------------------------------------------------------ *)
-qed_goal "up_lemma1" thy "z=Iup(x) ==> Iup(Ifup(LAM x.x)(z)) = z"
+qed_goal "up_lemma1" thy "z=Iup(x) ==> Iup(Ifup(LAM x. x)(z)) = z"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -111,8 +111,8 @@
(* ------------------------------------------------------------------------ *)
qed_goal "lub_up1a" thy
-"[|is_chain(Y);? i x.Y(i)=Iup(x)|] ==>\
-\ range(Y) <<| Iup(lub(range(%i.(Ifup (LAM x.x) (Y(i))))))"
+"[|is_chain(Y);? i x. Y(i)=Iup(x)|] ==>\
+\ range(Y) <<| Iup(lub(range(%i.(Ifup (LAM x. x) (Y(i))))))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -183,7 +183,7 @@
*)
qed_goal "cpo_up" thy
- "is_chain(Y::nat=>('a)u) ==> ? x.range(Y) <<|x"
+ "is_chain(Y::nat=>('a)u) ==> ? x. range(Y) <<|x"
(fn prems =>
[
(cut_facts_tac prems 1),