# HG changeset patch
# User wenzelm
# Date 1461703471 -7200
# Node ID 293ede07b7752feb39420d0948015eb3fcc7d51c
# Parent  3f577308551e4210ae54090d8094fe17084d1f65
some uses of 'obtain' with structure statement;

diff -r 3f577308551e -r 293ede07b775 src/HOL/Library/ContNotDenum.thy
--- a/src/HOL/Library/ContNotDenum.thy	Tue Apr 26 22:39:17 2016 +0200
+++ b/src/HOL/Library/ContNotDenum.thy	Tue Apr 26 22:44:31 2016 +0200
@@ -41,9 +41,10 @@
     by (auto simp add: not_le cong: conj_cong)
        (metis dense le_less_linear less_linear less_trans order_refl)
   then obtain i j where ij:
-    "\<And>a b c::real. a < b \<Longrightarrow> i a b c < j a b c"
-    "\<And>a b c. a < b \<Longrightarrow> {i a b c .. j a b c} \<subseteq> {a .. b}"
-    "\<And>a b c. a < b \<Longrightarrow> c \<notin> {i a b c .. j a b c}"
+      "a < b \<Longrightarrow> i a b c < j a b c"
+      "a < b \<Longrightarrow> {i a b c .. j a b c} \<subseteq> {a .. b}"
+      "a < b \<Longrightarrow> c \<notin> {i a b c .. j a b c}"
+    for a b c :: real
     by metis
 
   define ivl where "ivl =
@@ -78,7 +79,7 @@
     finally show "I 0 \<inter> (\<Inter>i\<in>S. I i) \<noteq> {}"
       by auto
   qed (auto simp: I_def)
-  then obtain x where "\<And>n. x \<in> I n"
+  then obtain x where "x \<in> I n" for n
     by blast
   moreover from \<open>surj f\<close> obtain j where "x = f j"
     by blast
diff -r 3f577308551e -r 293ede07b775 src/HOL/Library/Extended_Nonnegative_Real.thy
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Tue Apr 26 22:39:17 2016 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Tue Apr 26 22:44:31 2016 +0200
@@ -1483,7 +1483,7 @@
   case (real r)
   then have "\<forall>x. \<exists>q\<ge>0. g x \<le> c \<longrightarrow> (g x = ennreal q \<and> q \<le> r)"
     by (auto simp: le_ennreal_iff)
-  then obtain f where *: "\<And>x. g x \<le> c \<Longrightarrow> 0 \<le> f x" "\<And>x. g x \<le> c \<Longrightarrow> g x = ennreal (f x)" "\<And>x. g x \<le> c \<Longrightarrow> f x \<le> r"
+  then obtain f where *: "0 \<le> f x" "g x = ennreal (f x)" "f x \<le> r" if "g x \<le> c" for x
     by metis
   from ae have ae2: "\<forall>\<^sub>F x in F. c - g x = ennreal (r - f x) \<and> f x \<le> r \<and> g x = ennreal (f x) \<and> 0 \<le> f x"
   proof eventually_elim
diff -r 3f577308551e -r 293ede07b775 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Tue Apr 26 22:39:17 2016 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Tue Apr 26 22:44:31 2016 +0200
@@ -1696,7 +1696,7 @@
   shows "\<exists>x. (\<forall>y\<in>S. y \<le> x) \<and> (\<forall>z. (\<forall>y\<in>S. y \<le> z) \<longrightarrow> x \<le> z)"
 proof (cases "\<exists>x. \<forall>a\<in>S. a \<le> ereal x")
   case True
-  then obtain y where y: "\<And>a. a\<in>S \<Longrightarrow> a \<le> ereal y"
+  then obtain y where y: "a \<le> ereal y" if "a\<in>S" for a
     by auto
   then have "\<infinity> \<notin> S"
     by force
@@ -1705,7 +1705,7 @@
     case True
     with \<open>\<infinity> \<notin> S\<close> obtain x where x: "x \<in> S" "\<bar>x\<bar> \<noteq> \<infinity>"
       by auto
-    obtain s where s: "\<forall>x\<in>ereal -` S. x \<le> s" "\<And>z. (\<forall>x\<in>ereal -` S. x \<le> z) \<Longrightarrow> s \<le> z"
+    obtain s where s: "\<forall>x\<in>ereal -` S. x \<le> s" "(\<forall>x\<in>ereal -` S. x \<le> z) \<Longrightarrow> s \<le> z" for z
     proof (atomize_elim, rule complete_real)
       show "\<exists>x. x \<in> ereal -` S"
         using x by auto
@@ -1919,7 +1919,7 @@
   assumes *: "bdd_below A" "A \<noteq> {}"
   shows "ereal (Inf A) = (INF a:A. ereal a)"
 proof (rule ereal_Inf)
-  from * obtain l u where "\<And>x. x \<in> A \<Longrightarrow> l \<le> x" "u \<in> A"
+  from * obtain l u where "x \<in> A \<Longrightarrow> l \<le> x" "u \<in> A" for x
     by (auto simp: bdd_below_def)
   then have "l \<le> (INF x:A. ereal x)" "(INF x:A. ereal x) \<le> u"
     by (auto intro!: INF_greatest INF_lower)
@@ -2193,7 +2193,7 @@
     by (auto intro!: exI[of _ "\<lambda>_. -\<infinity>"] simp: bot_ereal_def)
 next
   assume "Sup A \<noteq> -\<infinity>"
-  then obtain l where "incseq l" and l: "\<And>i::nat. l i < Sup A" and l_Sup: "l \<longlonglongrightarrow> Sup A"
+  then obtain l where "incseq l" and l: "l i < Sup A" and l_Sup: "l \<longlonglongrightarrow> Sup A" for i :: nat
     by (auto dest: countable_approach)
 
   have "\<exists>f. \<forall>n. (f n \<in> A \<and> l n \<le> f n) \<and> (f n \<le> f (Suc n))"
@@ -2456,7 +2456,7 @@
   from \<open>open S\<close>
   have "open (ereal -` S)"
     by (rule ereal_openE)
-  then obtain e where "e > 0" and e: "\<And>y. dist y (real_of_ereal x) < e \<Longrightarrow> ereal y \<in> S"
+  then obtain e where "e > 0" and e: "dist y (real_of_ereal x) < e \<Longrightarrow> ereal y \<in> S" for y
     using assms unfolding open_dist by force
   show thesis
   proof (intro that subsetI)
@@ -2830,11 +2830,12 @@
   assume "open S" and "x \<in> S"
   then have "open (ereal -` S)"
     unfolding open_ereal_def by auto
-  with \<open>x \<in> S\<close> obtain r where "0 < r" and dist: "\<And>y. dist y rx < r \<Longrightarrow> ereal y \<in> S"
+  with \<open>x \<in> S\<close> obtain r where "0 < r" and dist: "dist y rx < r \<Longrightarrow> ereal y \<in> S" for y
     unfolding open_dist rx by auto
-  then obtain n where
-    upper: "\<And>N. n \<le> N \<Longrightarrow> u N < x + ereal r" and
-    lower: "\<And>N. n \<le> N \<Longrightarrow> x < u N + ereal r"
+  then obtain n
+    where upper: "u N < x + ereal r"
+      and lower: "x < u N + ereal r"
+      if "n \<le> N" for N
     using assms(2)[of "ereal r"] by auto
   show "\<exists>N. \<forall>n\<ge>N. u n \<in> S"
   proof (safe intro!: exI[of _ n])
diff -r 3f577308551e -r 293ede07b775 src/HOL/Library/Fun_Lexorder.thy
--- a/src/HOL/Library/Fun_Lexorder.thy	Tue Apr 26 22:39:17 2016 +0200
+++ b/src/HOL/Library/Fun_Lexorder.thy	Tue Apr 26 22:44:31 2016 +0200
@@ -24,9 +24,9 @@
   assumes "less_fun f g"
   shows "\<not> less_fun g f"
 proof
-  from assms obtain k1 where k1: "f k1 < g k1" "\<And>k'. k' < k1 \<Longrightarrow> f k' = g k'"
+  from assms obtain k1 where k1: "f k1 < g k1" "k' < k1 \<Longrightarrow> f k' = g k'" for k'
     by (blast elim!: less_funE) 
-  assume "less_fun g f" then obtain k2 where k2: "g k2 < f k2" "\<And>k'. k' < k2 \<Longrightarrow> g k' = f k'"
+  assume "less_fun g f" then obtain k2 where k2: "g k2 < f k2" "k' < k2 \<Longrightarrow> g k' = f k'" for k'
     by (blast elim!: less_funE) 
   show False proof (cases k1 k2 rule: linorder_cases)
     case equal with k1 k2 show False by simp
@@ -52,9 +52,9 @@
   assumes "less_fun f g" and "less_fun g h"
   shows "less_fun f h"
 proof (rule less_funI)
-  from \<open>less_fun f g\<close> obtain k1 where k1: "f k1 < g k1" "\<And>k'. k' < k1 \<Longrightarrow> f k' = g k'"
-    by (blast elim!: less_funE) 
-  from \<open>less_fun g h\<close> obtain k2 where k2: "g k2 < h k2" "\<And>k'. k' < k2 \<Longrightarrow> g k' = h k'"
+  from \<open>less_fun f g\<close> obtain k1 where k1: "f k1 < g k1" "k' < k1 \<Longrightarrow> f k' = g k'" for k'
+    by (blast elim!: less_funE)                          
+  from \<open>less_fun g h\<close> obtain k2 where k2: "g k2 < h k2" "k' < k2 \<Longrightarrow> g k' = h k'" for k'
     by (blast elim!: less_funE) 
   show "\<exists>k. f k < h k \<and> (\<forall>k'<k. f k' = h k')"
   proof (cases k1 k2 rule: linorder_cases)
diff -r 3f577308551e -r 293ede07b775 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Tue Apr 26 22:39:17 2016 +0200
+++ b/src/HOL/Library/FuncSet.thy	Tue Apr 26 22:44:31 2016 +0200
@@ -96,9 +96,9 @@
   assume "f \<in> (\<Pi> i\<in>I. \<Union>n. A n i)"
   then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i"
     by auto
-  from bchoice[OF this] obtain n where n: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> (A (n i) i)"
+  from bchoice[OF this] obtain n where n: "f i \<in> A (n i) i" if "i \<in> I" for i
     by auto
-  obtain k where k: "\<And>i. i \<in> I \<Longrightarrow> n i \<le> k"
+  obtain k where k: "n i \<le> k" if "i \<in> I" for i
     using \<open>finite I\<close> finite_nat_set_iff_bounded_le[of "n`I"] by auto
   have "f \<in> Pi I (A k)"
   proof (intro Pi_I)
diff -r 3f577308551e -r 293ede07b775 src/HOL/Library/Function_Growth.thy
--- a/src/HOL/Library/Function_Growth.thy	Tue Apr 26 22:39:17 2016 +0200
+++ b/src/HOL/Library/Function_Growth.thy	Tue Apr 26 22:44:31 2016 +0200
@@ -163,7 +163,7 @@
     and "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * f m < g m"
 proof -
   from assms have "f \<lesssim> g" and "\<not> g \<lesssim> f" by (simp_all add: less_fun_def)
-  from \<open>f \<lesssim> g\<close> obtain n c where *:"c > 0" "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m"
+  from \<open>f \<lesssim> g\<close> obtain n c where *:"c > 0" "m > n \<Longrightarrow> f m \<le> c * g m" for m
     by (rule less_eq_funE) blast
   { fix c n :: nat
     assume "c > 0"
@@ -202,8 +202,8 @@
   shows "f \<prec> g"
 proof (rule less_funI)
   have "1 > (0::nat)" by simp
-  from assms \<open>1 > 0\<close> have "\<exists>n. \<forall>m>n. 1 * f m < g m" .
-  then obtain n where *: "\<And>m. m > n \<Longrightarrow> 1 * f m < g m" by blast
+  with assms [OF this] obtain n where *: "m > n \<Longrightarrow> 1 * f m < g m" for m
+    by blast
   have "\<forall>m>n. f m \<le> 1 * g m"
   proof (rule allI, rule impI)
     fix m
@@ -214,7 +214,7 @@
   with \<open>1 > 0\<close> show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" by blast
   fix c n :: nat
   assume "c > 0"
-  with assms obtain q where "\<And>m. m > q \<Longrightarrow> c * f m < g m" by blast
+  with assms obtain q where "m > q \<Longrightarrow> c * f m < g m" for m by blast
   then have "c * f (Suc (q + n)) < g (Suc (q + n))" by simp
   moreover have "Suc (q + n) > n" by simp
   ultimately show "\<exists>m>n. c * f m < g m" by blast
diff -r 3f577308551e -r 293ede07b775 src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Apr 26 22:39:17 2016 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Apr 26 22:44:31 2016 +0200
@@ -312,7 +312,7 @@
   assumes ep: "e > 0"
   shows "\<exists>d >0. \<forall>w. 0 < norm (w - z) \<and> norm (w - z) < d \<longrightarrow> norm (poly p w - poly p z) < e"
 proof -
-  obtain q where q: "degree q = degree p" "\<And>x. poly q x = poly p (z + x)"
+  obtain q where q: "degree q = degree p" "poly q x = poly p (z + x)" for x
   proof
     show "degree (offset_poly p z) = degree p"
       by (rule degree_offset_poly)
@@ -329,7 +329,7 @@
   next
     case (pCons c cs)
     from poly_bound_exists[of 1 "cs"]
-    obtain m where m: "m > 0" "\<And>z. norm z \<le> 1 \<Longrightarrow> norm (poly cs z) \<le> m"
+    obtain m where m: "m > 0" "norm z \<le> 1 \<Longrightarrow> norm (poly cs z) \<le> m" for z
       by blast
     from ep m(1) have em0: "e/m > 0"
       by (simp add: field_simps)
@@ -535,12 +535,14 @@
   proof (cases "cs = 0")
     case False
     from poly_infinity[OF False, of "cmod (poly (pCons c cs) 0)" c]
-    obtain r where r: "\<And>z. r \<le> cmod z \<Longrightarrow> cmod (poly (pCons c cs) 0) \<le> cmod (poly (pCons c cs) z)"
+    obtain r where r: "cmod (poly (pCons c cs) 0) \<le> cmod (poly (pCons c cs) z)"
+      if "r \<le> cmod z" for z
       by blast
     have ath: "\<And>z r. r \<le> cmod z \<or> cmod z \<le> \<bar>r\<bar>"
       by arith
     from poly_minimum_modulus_disc[of "\<bar>r\<bar>" "pCons c cs"]
-    obtain v where v: "\<And>w. cmod w \<le> \<bar>r\<bar> \<Longrightarrow> cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) w)"
+    obtain v where v: "cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) w)"
+      if "cmod w \<le> \<bar>r\<bar>" for w
       by blast
     have "cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) z)" if z: "r \<le> cmod z" for z
       using v[of 0] r[OF z] by simp
diff -r 3f577308551e -r 293ede07b775 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Apr 26 22:39:17 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Tue Apr 26 22:44:31 2016 +0200
@@ -2075,7 +2075,7 @@
     "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
 proof -
   from assms obtain a M0 K where "M = M0 + {#a#}" "N = M0 + K"
-    "\<And>b. b \<in># K \<Longrightarrow> b < a" by (blast elim: mult1E)
+    "b \<in># K \<Longrightarrow> b < a" for b by (blast elim: mult1E)
   moreover from this(3) [of a] have "a \<notin># K" by auto
   ultimately show thesis by (auto intro: that)
 qed
diff -r 3f577308551e -r 293ede07b775 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Tue Apr 26 22:39:17 2016 +0200
+++ b/src/HOL/Library/Polynomial.thy	Tue Apr 26 22:44:31 2016 +0200
@@ -3353,7 +3353,7 @@
   fix p assume rat: "\<forall>i. coeff p i \<in> \<rat>" and root: "poly p x = 0" and nz: "p \<noteq> 0"
   define cs where "cs = coeffs p"
   from rat have "\<forall>c\<in>range (coeff p). \<exists>c'. c = of_rat c'" unfolding Rats_def by blast
-  then obtain f where f: "\<And>i. coeff p i = of_rat (f (coeff p i))" 
+  then obtain f where f: "coeff p i = of_rat (f (coeff p i))" for i
     by (subst (asm) bchoice_iff) blast
   define cs' where "cs' = map (quotient_of \<circ> f) (coeffs p)"
   define d where "d = Lcm (set (map snd cs'))"
@@ -3392,9 +3392,8 @@
   moreover from root have "poly p' x = 0" by (simp add: p'_def)
   ultimately show "algebraic x" unfolding algebraic_def by blast
 next
-
   assume "algebraic x"
-  then obtain p where p: "\<And>i. coeff p i \<in> \<int>" "poly p x = 0" "p \<noteq> 0" 
+  then obtain p where p: "coeff p i \<in> \<int>" "poly p x = 0" "p \<noteq> 0" for i
     by (force simp: algebraic_def)
   moreover have "coeff p i \<in> \<int> \<Longrightarrow> coeff p i \<in> \<rat>" for i by (elim Ints_cases) simp
   ultimately show  "(\<exists>p. (\<forall>i. coeff p i \<in> \<rat>) \<and> p \<noteq> 0 \<and> poly p x = 0)" by auto
diff -r 3f577308551e -r 293ede07b775 src/HOL/Library/Ramsey.thy
--- a/src/HOL/Library/Ramsey.thy	Tue Apr 26 22:39:17 2016 +0200
+++ b/src/HOL/Library/Ramsey.thy	Tue Apr 26 22:44:31 2016 +0200
@@ -231,8 +231,8 @@
       qed
     qed
     from dependent_choice [OF transr propr0 proprstep]
-    obtain g where pg: "!!n::nat.  ?propr (g n)"
-      and rg: "!!n m. n<m ==> (g n, g m) \<in> ?ramr" by blast
+    obtain g where pg: "?propr (g n)" and rg: "n<m ==> (g n, g m) \<in> ?ramr" for n m :: nat
+      by blast
     let ?gy = "fst o g"
     let ?gt = "snd o snd o g"
     have rangeg: "\<exists>k. range ?gt \<subseteq> {..<k}"
diff -r 3f577308551e -r 293ede07b775 src/HOL/Number_Theory/Factorial_Ring.thy
--- a/src/HOL/Number_Theory/Factorial_Ring.thy	Tue Apr 26 22:39:17 2016 +0200
+++ b/src/HOL/Number_Theory/Factorial_Ring.thy	Tue Apr 26 22:44:31 2016 +0200
@@ -609,12 +609,13 @@
   next
     case False then have "a \<noteq> 0" and "b \<noteq> 0" and "c \<noteq> 0"
       by simp_all
-    then obtain A B C where fact:
-      "factorization a = Some A" "factorization b = Some B" "factorization c = Some C"
+    then obtain A B C
+    where fact: "factorization a = Some A" "factorization b = Some B" "factorization c = Some C"
       and norm: "normalize a = msetprod A" "normalize b = msetprod B" "normalize c = msetprod C"
-      and A: "0 \<notin># A" "\<And>p. p \<in># A \<Longrightarrow> normalize p = p" "\<And>p. p \<in># A \<Longrightarrow> is_prime p"
-      and B: "0 \<notin># B" "\<And>p. p \<in># B \<Longrightarrow> normalize p = p" "\<And>p. p \<in># B \<Longrightarrow> is_prime p"
-      and C: "0 \<notin># C" "\<And>p. p \<in># C \<Longrightarrow> normalize p = p" "\<And>p. p \<in># C \<Longrightarrow> is_prime p"
+      and A: "0 \<notin># A" "p \<in># A \<Longrightarrow> normalize p = p" "p \<in># A \<Longrightarrow> is_prime p"
+      and B: "0 \<notin># B" "p \<in># B \<Longrightarrow> normalize p = p" "p \<in># B \<Longrightarrow> is_prime p"
+      and C: "0 \<notin># C" "p \<in># C \<Longrightarrow> normalize p = p" "p \<in># C \<Longrightarrow> is_prime p"
+      for p
       by (blast elim!: factorizationE)
     moreover from that have "normalize c dvd normalize a" and "normalize c dvd normalize b"
       by simp_all
diff -r 3f577308551e -r 293ede07b775 src/HOL/Proofs/Lambda/WeakNorm.thy
--- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Tue Apr 26 22:39:17 2016 +0200
+++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Tue Apr 26 22:44:31 2016 +0200
@@ -40,9 +40,9 @@
     by (rule types_snocE)
   from snoc have "listall ?R bs" by simp
   with bs have "\<exists>bs'. ?ex Vs bs bs'" by (rule snoc)
-  then obtain bs' where
-    bsred: "\<And>j. Var j \<degree>\<degree> map (\<lambda>t. f (t[u/i])) bs \<rightarrow>\<^sub>\<beta>\<^sup>* Var j \<degree>\<degree> map f bs'"
-    and bsNF: "\<And>j. NF (Var j \<degree>\<degree> map f bs')" by iprover
+  then obtain bs' where bsred: "Var j \<degree>\<degree> map (\<lambda>t. f (t[u/i])) bs \<rightarrow>\<^sub>\<beta>\<^sup>* Var j \<degree>\<degree> map f bs'"
+    and bsNF: "NF (Var j \<degree>\<degree> map f bs')" for j
+    by iprover
   from snoc have "?R b" by simp
   with bT and uNF and uT have "\<exists>b'. b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b' \<and> NF b'"
     by iprover
diff -r 3f577308551e -r 293ede07b775 src/HOL/ex/Gauge_Integration.thy
--- a/src/HOL/ex/Gauge_Integration.thy	Tue Apr 26 22:39:17 2016 +0200
+++ b/src/HOL/ex/Gauge_Integration.thy	Tue Apr 26 22:44:31 2016 +0200
@@ -133,7 +133,7 @@
   proof (cases "b < x")
     case True
     with 2 obtain N where *: "N < length D"
-      and **: "\<And> d t e. D ! N = (d,t,e) \<Longrightarrow> d < x \<and> x \<le> e" by auto
+      and **: "D ! N = (d,t,e) \<Longrightarrow> d < x \<and> x \<le> e" for d t e by auto
     hence "Suc N < length ((a,t,b)#D) \<and>
            (\<forall> d t' e. ((a,t,b)#D) ! Suc N = (d,t',e) \<longrightarrow> d < x \<and> x \<le> e)" by auto
     thus ?thesis by auto
@@ -372,11 +372,11 @@
   hence "a < b" and "b < c" by auto
 
   obtain \<delta>1 where \<delta>1_gauge: "gauge {a..b} \<delta>1"
-    and I1: "\<And> D. fine \<delta>1 (a,b) D \<Longrightarrow> \<bar> rsum D f - x1 \<bar> < (\<epsilon> / 2)"
+    and I1: "fine \<delta>1 (a,b) D \<Longrightarrow> \<bar> rsum D f - x1 \<bar> < (\<epsilon> / 2)" for D
     using IntegralE [OF \<open>Integral (a, b) f x1\<close> \<open>0 < \<epsilon>/2\<close>] by auto
 
   obtain \<delta>2 where \<delta>2_gauge: "gauge {b..c} \<delta>2"
-    and I2: "\<And> D. fine \<delta>2 (b,c) D \<Longrightarrow> \<bar> rsum D f - x2 \<bar> < (\<epsilon> / 2)"
+    and I2: "fine \<delta>2 (b,c) D \<Longrightarrow> \<bar> rsum D f - x2 \<bar> < (\<epsilon> / 2)" for D
     using IntegralE [OF \<open>Integral (b, c) f x2\<close> \<open>0 < \<epsilon>/2\<close>] by auto
 
   define \<delta> where "\<delta> x =
@@ -541,7 +541,7 @@
     then have "\<forall>r>0. \<exists>s>0. \<forall>z. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < r"
       by (simp add: DERIV_iff2 LIM_eq)
     with \<open>0 < e\<close> obtain s
-    where "\<And>z. z \<noteq> x \<Longrightarrow> \<bar>z - x\<bar> < s \<Longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < e/2" and "0 < s"
+    where "z \<noteq> x \<Longrightarrow> \<bar>z - x\<bar> < s \<Longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < e/2" and "0 < s" for z
       by (drule_tac x="e/2" in spec, auto)
     with strad1 [of x s f f' e] have strad:
         "\<And>z. \<bar>z - x\<bar> < s \<Longrightarrow> \<bar>f z - f x - f' x * (z - x)\<bar> \<le> e/2 * \<bar>z - x\<bar>"
@@ -586,8 +586,8 @@
 
     from lemma_straddle [OF f' this]
     obtain \<delta> where "gauge {a..b} \<delta>"
-      and \<delta>: "\<And>x u v. \<lbrakk>a \<le> u; u \<le> x; x \<le> v; v \<le> b; v - u < \<delta> x\<rbrakk> \<Longrightarrow>
-           \<bar>f v - f u - f' x * (v - u)\<bar> \<le> e * (v - u) / (b - a)" by auto
+      and \<delta>: "\<lbrakk>a \<le> u; u \<le> x; x \<le> v; v \<le> b; v - u < \<delta> x\<rbrakk> \<Longrightarrow>
+           \<bar>f v - f u - f' x * (v - u)\<bar> \<le> e * (v - u) / (b - a)" for x u v by auto
 
     have "\<forall>D. fine \<delta> (a, b) D \<longrightarrow> \<bar>rsum D f' - (f b - f a)\<bar> \<le> e"
     proof (clarify)