src/HOL/Library/Liminf_Limsup.thy
changeset 53374 a14d2a854c02
parent 53216 ad2e09c30aa8
child 53381 355a4cac5440
--- a/src/HOL/Library/Liminf_Limsup.thy	Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Library/Liminf_Limsup.thy	Tue Sep 03 01:12:40 2013 +0200
@@ -171,8 +171,8 @@
     have "\<exists>P. eventually P F \<and> y < INFI (Collect P) X"
     proof cases
       assume "\<exists>z. y < z \<and> z < C"
-      then guess z ..
-      moreover then have "z \<le> INFI {x. z < X x} X"
+      then guess z .. note z = this
+      moreover from z have "z \<le> INFI {x. z < X x} X"
         by (auto intro!: INF_greatest)
       ultimately show ?thesis
         using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
@@ -203,7 +203,7 @@
   show "f0 \<le> y"
   proof cases
     assume "\<exists>z. y < z \<and> z < f0"
-    then guess z ..
+    then obtain z where "y < z \<and> z < f0" ..
     moreover have "z \<le> INFI {x. z < f x} f"
       by (rule INF_greatest) simp
     ultimately show ?thesis