--- a/src/HOLCF/Up3.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Up3.ML Fri Oct 10 19:02:28 1997 +0200
@@ -274,7 +274,7 @@
]);
-qed_goal "up_lemma2" thy " (? x.z = up`x) = (z~=UU)"
+qed_goal "up_lemma2" thy " (? x. z = up`x) = (z~=UU)"
(fn prems =>
[
(rtac iffI 1),
@@ -317,7 +317,7 @@
qed_goal "thelub_up3" thy
"is_chain(Y) ==> lub(range(Y)) = UU |\
-\ lub(range(Y)) = up`(lub(range(%i. fup`(LAM x.x)`(Y i))))"
+\ lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))"
(fn prems =>
[
(cut_facts_tac prems 1),