# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1531656931 -3600
# Node ID db0980691ef4f597888cb10752c59500d1c698e5
# Parent  ae4373f3d8d3a945d90df29ceb4a482b98235ea9
more de-applying and a fix

diff -r ae4373f3d8d3 -r db0980691ef4 src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sun Jul 15 10:41:57 2018 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sun Jul 15 13:15:31 2018 +0100
@@ -6919,7 +6919,7 @@
       then have "f field_differentiable at a"
         using holfb \<open>0 < e\<close> holomorphic_on_imp_differentiable_at by auto
       with True show ?thesis
-        by (auto simp: continuous_at DERIV_iff2 simp flip: DERIV_deriv_iff_field_differentiable
+        by (auto simp: continuous_at has_field_derivative_iff simp flip: DERIV_deriv_iff_field_differentiable
                 elim: rev_iffD1 [OF _ LIM_equal])
     next
       case False with 2 that show ?thesis
diff -r ae4373f3d8d3 -r db0980691ef4 src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy	Sun Jul 15 10:41:57 2018 +0100
+++ b/src/HOL/Analysis/Further_Topology.thy	Sun Jul 15 13:15:31 2018 +0100
@@ -3987,7 +3987,7 @@
   have "g field_differentiable at z within S" if "f field_differentiable at z within S" "z \<in> S" for z
   proof -
     obtain f' where f': "((\<lambda>y. (f y - f z) / (y - z)) \<longlongrightarrow> f') (at z within S)"
-      using \<open>f field_differentiable at z within S\<close> by (auto simp: field_differentiable_def DERIV_iff2)
+      using \<open>f field_differentiable at z within S\<close> by (auto simp: field_differentiable_def has_field_derivative_iff)
     then have ee: "((\<lambda>x. (exp(g x) - exp(g z)) / (x - z)) \<longlongrightarrow> f') (at z within S)"
       by (simp add: feq \<open>z \<in> S\<close> Lim_transform_within [OF _ zero_less_one])
     have "(((\<lambda>y. if y = g z then exp (g z) else (exp y - exp (g z)) / (y - g z)) \<circ> g) \<longlongrightarrow> exp (g z))
@@ -4013,7 +4013,7 @@
     then have "((\<lambda>y. (g y - g z) / (y - z)) \<longlongrightarrow> f' / exp (g z)) (at z within S)"
       by (auto intro!: Lim_transform_eventually [OF _ tendsto_divide [OF ee dd]])
     then show ?thesis
-      by (auto simp: field_differentiable_def DERIV_iff2)
+      by (auto simp: field_differentiable_def has_field_derivative_iff)
   qed
   then have "g holomorphic_on S"
     using holf holomorphic_on_def by auto
@@ -4035,7 +4035,7 @@
   have "g field_differentiable at z within S" if "f field_differentiable at z within S" "z \<in> S" for z
   proof -
     obtain f' where f': "((\<lambda>y. (f y - f z) / (y - z)) \<longlongrightarrow> f') (at z within S)"
-      using \<open>f field_differentiable at z within S\<close> by (auto simp: field_differentiable_def DERIV_iff2)
+      using \<open>f field_differentiable at z within S\<close> by (auto simp: field_differentiable_def has_field_derivative_iff)
     then have ee: "((\<lambda>x. (exp(g x) - exp(g z)) / (x - z)) \<longlongrightarrow> f') (at z within S)"
       by (simp add: feq \<open>z \<in> S\<close> Lim_transform_within [OF _ zero_less_one])
     have "(((\<lambda>y. if y = g z then exp (g z) else (exp y - exp (g z)) / (y - g z)) \<circ> g) \<longlongrightarrow> exp (g z))
@@ -4061,7 +4061,7 @@
     then have "((\<lambda>y. (g y - g z) / (y - z)) \<longlongrightarrow> f' / exp (g z)) (at z within S)"
       by (auto intro!: Lim_transform_eventually [OF _ tendsto_divide [OF ee dd]])
     then show ?thesis
-      by (auto simp: field_differentiable_def DERIV_iff2)
+      by (auto simp: field_differentiable_def has_field_derivative_iff)
   qed
   then have "g holomorphic_on S"
     using holf holomorphic_on_def by auto
diff -r ae4373f3d8d3 -r db0980691ef4 src/HOL/Analysis/Riemann_Mapping.thy
--- a/src/HOL/Analysis/Riemann_Mapping.thy	Sun Jul 15 10:41:57 2018 +0100
+++ b/src/HOL/Analysis/Riemann_Mapping.thy	Sun Jul 15 13:15:31 2018 +0100
@@ -1363,7 +1363,7 @@
         using \<open>z \<in> S\<close> contg continuous_on_eq_continuous_at isCont_def openS apply blast
         by (simp add: \<open>g z \<noteq> 0\<close>)
       then have "(g has_field_derivative deriv f z / (g z + g z)) (at z)"
-        unfolding DERIV_iff2
+        unfolding has_field_derivative_iff
       proof (rule Lim_transform_within_open)
         show "open (ball z \<delta> \<inter> S)"
           by (simp add: openS open_Int)
diff -r ae4373f3d8d3 -r db0980691ef4 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Sun Jul 15 10:41:57 2018 +0100
+++ b/src/HOL/Deriv.thy	Sun Jul 15 13:15:31 2018 +0100
@@ -93,11 +93,7 @@
 lemma (in bounded_linear) has_derivative:
   "(g has_derivative g') F \<Longrightarrow> ((\<lambda>x. f (g x)) has_derivative (\<lambda>x. f (g' x))) F"
   unfolding has_derivative_def
-  apply safe
-   apply (erule bounded_linear_compose [OF bounded_linear])
-  apply (drule tendsto)
-  apply (simp add: scaleR diff add zero)
-  done
+  by (auto simp add: bounded_linear_compose [OF bounded_linear] scaleR diff dest: tendsto)
 
 lemmas has_derivative_scaleR_right [derivative_intros] =
   bounded_linear.has_derivative [OF bounded_linear_scaleR_right]
@@ -157,15 +153,18 @@
 
 lemma field_has_derivative_at:
   fixes x :: "'a::real_normed_field"
-  shows "(f has_derivative ( * ) D) (at x) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D"
-  apply (unfold has_derivative_at)
-  apply (simp add: bounded_linear_mult_right)
-  apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric])
-  apply (subst diff_divide_distrib)
-  apply (subst times_divide_eq_left [symmetric])
-  apply (simp cong: LIM_cong)
-  apply (simp add: tendsto_norm_zero_iff LIM_zero_iff)
-  done
+  shows "(f has_derivative ( * ) D) (at x) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D" (is "?lhs = ?rhs")
+proof -
+  have "?lhs = (\<lambda>h. norm (f (x + h) - f x - D * h) / norm h) \<midarrow>0 \<rightarrow> 0"
+    by (simp add: bounded_linear_mult_right has_derivative_at)
+  also have "... = (\<lambda>y. norm ((f (x + y) - f x - D * y) / y)) \<midarrow>0\<rightarrow> 0"
+    by (simp cong: LIM_cong flip: nonzero_norm_divide)
+  also have "... = (\<lambda>y. norm ((f (x + y) - f x) / y - D / y * y)) \<midarrow>0\<rightarrow> 0"
+    by (simp only: diff_divide_distrib times_divide_eq_left [symmetric])
+  also have "... = ?rhs"
+    by (simp add: tendsto_norm_zero_iff LIM_zero_iff cong: LIM_cong)
+  finally show ?thesis .
+qed
 
 lemma has_derivativeI:
   "bounded_linear f' \<Longrightarrow>
@@ -414,8 +413,8 @@
 
 lemma has_derivative_prod[simp, derivative_intros]:
   fixes f :: "'i \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::real_normed_field"
-  shows "(\<And>i. i \<in> I \<Longrightarrow> (f i has_derivative f' i) (at x within s)) \<Longrightarrow>
-    ((\<lambda>x. \<Prod>i\<in>I. f i x) has_derivative (\<lambda>y. \<Sum>i\<in>I. f' i y * (\<Prod>j\<in>I - {i}. f j x))) (at x within s)"
+  shows "(\<And>i. i \<in> I \<Longrightarrow> (f i has_derivative f' i) (at x within S)) \<Longrightarrow>
+    ((\<lambda>x. \<Prod>i\<in>I. f i x) has_derivative (\<lambda>y. \<Sum>i\<in>I. f' i y * (\<Prod>j\<in>I - {i}. f j x))) (at x within S)"
 proof (induct I rule: infinite_finite_induct)
   case infinite
   then show ?case by simp
@@ -425,7 +424,7 @@
 next
   case (insert i I)
   let ?P = "\<lambda>y. f i x * (\<Sum>i\<in>I. f' i y * (\<Prod>j\<in>I - {i}. f j x)) + (f' i y) * (\<Prod>i\<in>I. f i x)"
-  have "((\<lambda>x. f i x * (\<Prod>i\<in>I. f i x)) has_derivative ?P) (at x within s)"
+  have "((\<lambda>x. f i x * (\<Prod>i\<in>I. f i x)) has_derivative ?P) (at x within S)"
     using insert by (intro has_derivative_mult) auto
   also have "?P = (\<lambda>y. \<Sum>i'\<in>insert i I. f' i' y * (\<Prod>j\<in>insert i I - {i'}. f j x))"
     using insert(1,2)
@@ -436,69 +435,56 @@
 
 lemma has_derivative_power[simp, derivative_intros]:
   fixes f :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
-  assumes f: "(f has_derivative f') (at x within s)"
-  shows "((\<lambda>x. f x^n) has_derivative (\<lambda>y. of_nat n * f' y * f x^(n - 1))) (at x within s)"
+  assumes f: "(f has_derivative f') (at x within S)"
+  shows "((\<lambda>x. f x^n) has_derivative (\<lambda>y. of_nat n * f' y * f x^(n - 1))) (at x within S)"
   using has_derivative_prod[OF f, of "{..< n}"] by (simp add: prod_constant ac_simps)
 
 lemma has_derivative_inverse':
   fixes x :: "'a::real_normed_div_algebra"
   assumes x: "x \<noteq> 0"
-  shows "(inverse has_derivative (\<lambda>h. - (inverse x * h * inverse x))) (at x within s)"
-    (is "(?inv has_derivative ?f) _")
+  shows "(inverse has_derivative (\<lambda>h. - (inverse x * h * inverse x))) (at x within S)"
+    (is "(_ has_derivative ?f) _")
 proof (rule has_derivativeI_sandwich)
-  show "bounded_linear (\<lambda>h. - (?inv x * h * ?inv x))"
-    apply (rule bounded_linear_minus)
-    apply (rule bounded_linear_mult_const)
-    apply (rule bounded_linear_const_mult)
-    apply (rule bounded_linear_ident)
-    done
+  show "bounded_linear (\<lambda>h. - (inverse x * h * inverse x))"
+    by (simp add: bounded_linear_minus bounded_linear_mult_const bounded_linear_mult_right)
   show "0 < norm x" using x by simp
-  show "((\<lambda>y. norm (?inv y - ?inv x) * norm (?inv x)) \<longlongrightarrow> 0) (at x within s)"
-    apply (rule tendsto_mult_left_zero)
-    apply (rule tendsto_norm_zero)
-    apply (rule LIM_zero)
-    apply (rule tendsto_inverse)
-     apply (rule tendsto_ident_at)
-    apply (rule x)
-    done
+  have "(inverse \<longlongrightarrow> inverse x) (at x within S)"
+    using tendsto_inverse tendsto_ident_at x by auto
+  then show "((\<lambda>y. norm (inverse y - inverse x) * norm (inverse x)) \<longlongrightarrow> 0) (at x within S)"
+    by (simp add: LIM_zero_iff tendsto_mult_left_zero tendsto_norm_zero)
 next
   fix y :: 'a
   assume h: "y \<noteq> x" "dist y x < norm x"
   then have "y \<noteq> 0" by auto
-  have "norm (?inv y - ?inv x - ?f (y -x)) / norm (y - x) =
-      norm ((?inv y - ?inv x) * (y - x) * ?inv x) / norm (y - x)"
-    apply (subst inverse_diff_inverse [OF \<open>y \<noteq> 0\<close> x])
-    apply (subst minus_diff_minus)
-    apply (subst norm_minus_cancel)
-    apply (simp add: left_diff_distrib)
-    done
-  also have "\<dots> \<le> norm (?inv y - ?inv x) * norm (y - x) * norm (?inv x) / norm (y - x)"
-    apply (rule divide_right_mono [OF _ norm_ge_zero])
-    apply (rule order_trans [OF norm_mult_ineq])
-    apply (rule mult_right_mono [OF _ norm_ge_zero])
-    apply (rule norm_mult_ineq)
-    done
-  also have "\<dots> = norm (?inv y - ?inv x) * norm (?inv x)"
+  have "norm (inverse y - inverse x - ?f (y -x)) / norm (y - x) 
+        = norm (- (inverse y * (y - x) * inverse x - inverse x * (y - x) * inverse x)) /
+                norm (y - x)"
+    by (simp add: \<open>y \<noteq> 0\<close> inverse_diff_inverse x)
+  also have "... = norm ((inverse y - inverse x) * (y - x) * inverse x) / norm (y - x)"
+    by (simp add: left_diff_distrib norm_minus_commute)
+  also have "\<dots> \<le> norm (inverse y - inverse x) * norm (y - x) * norm (inverse x) / norm (y - x)"
+    by (simp add: norm_mult)
+  also have "\<dots> = norm (inverse y - inverse x) * norm (inverse x)"
     by simp
-  finally show "norm (?inv y - ?inv x - ?f (y -x)) / norm (y - x) \<le>
-    norm (?inv y - ?inv x) * norm (?inv x)" .
+  finally show "norm (inverse y - inverse x - ?f (y -x)) / norm (y - x) \<le>
+    norm (inverse y - inverse x) * norm (inverse x)" .
 qed
 
 lemma has_derivative_inverse[simp, derivative_intros]:
   fixes f :: "_ \<Rightarrow> 'a::real_normed_div_algebra"
   assumes x:  "f x \<noteq> 0"
-    and f: "(f has_derivative f') (at x within s)"
+    and f: "(f has_derivative f') (at x within S)"
   shows "((\<lambda>x. inverse (f x)) has_derivative (\<lambda>h. - (inverse (f x) * f' h * inverse (f x))))
-    (at x within s)"
+    (at x within S)"
   using has_derivative_compose[OF f has_derivative_inverse', OF x] .
 
 lemma has_derivative_divide[simp, derivative_intros]:
   fixes f :: "_ \<Rightarrow> 'a::real_normed_div_algebra"
-  assumes f: "(f has_derivative f') (at x within s)"
-    and g: "(g has_derivative g') (at x within s)"
+  assumes f: "(f has_derivative f') (at x within S)"
+    and g: "(g has_derivative g') (at x within S)"
   assumes x: "g x \<noteq> 0"
   shows "((\<lambda>x. f x / g x) has_derivative
-                (\<lambda>h. - f x * (inverse (g x) * g' h * inverse (g x)) + f' h / g x)) (at x within s)"
+                (\<lambda>h. - f x * (inverse (g x) * g' h * inverse (g x)) + f' h / g x)) (at x within S)"
   using has_derivative_mult[OF f has_derivative_inverse[OF x g]]
   by (simp add: field_simps)
 
@@ -507,10 +493,10 @@
 
 lemma has_derivative_divide'[derivative_intros]:
   fixes f :: "_ \<Rightarrow> 'a::real_normed_field"
-  assumes f: "(f has_derivative f') (at x within s)"
-    and g: "(g has_derivative g') (at x within s)"
+  assumes f: "(f has_derivative f') (at x within S)"
+    and g: "(g has_derivative g') (at x within S)"
     and x: "g x \<noteq> 0"
-  shows "((\<lambda>x. f x / g x) has_derivative (\<lambda>h. (f' h * g x - f x * g' h) / (g x * g x))) (at x within s)"
+  shows "((\<lambda>x. f x / g x) has_derivative (\<lambda>h. (f' h * g x - f x * g' h) / (g x * g x))) (at x within S)"
 proof -
   have "f' h / g x - f x * (inverse (g x) * g' h * inverse (g x)) =
       (f' h * g x - f x * g' h) / (g x * g x)" for h
@@ -550,12 +536,12 @@
         by (auto simp add: F.zero)
       with ** have "0 < ?r h"
         by simp
-      from LIM_D [OF * this] obtain s
-        where s: "0 < s" and r: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < s \<Longrightarrow> ?r x < ?r h"
+      from LIM_D [OF * this] obtain S
+        where S: "0 < S" and r: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < S \<Longrightarrow> ?r x < ?r h"
         by auto
-      from dense [OF s] obtain t where t: "0 < t \<and> t < s" ..
+      from dense [OF S] obtain t where t: "0 < t \<and> t < S" ..
       let ?x = "scaleR (t / norm h) h"
-      have "?x \<noteq> 0" and "norm ?x < s"
+      have "?x \<noteq> 0" and "norm ?x < S"
         using t h by simp_all
       then have "?r ?x < ?r h"
         by (rule r)
@@ -711,12 +697,15 @@
 lemma has_field_derivative_iff:
   "(f has_field_derivative D) (at x within S) \<longleftrightarrow>
     ((\<lambda>y. (f y - f x) / (y - x)) \<longlongrightarrow> D) (at x within S)"
-  apply (simp add: has_field_derivative_def has_derivative_iff_norm bounded_linear_mult_right
-      LIM_zero_iff[symmetric, of _ D])
-  apply (subst (2) tendsto_norm_zero_iff[symmetric])
-  apply (rule filterlim_cong)
-    apply (simp_all add: eventually_at_filter field_simps nonzero_norm_divide)
-  done
+proof -
+  have "((\<lambda>y. norm (f y - f x - D * (y - x)) / norm (y - x)) \<longlongrightarrow> 0) (at x within S) 
+      = ((\<lambda>y. (f y - f x) / (y - x) - D) \<longlongrightarrow> 0) (at x within S)"
+    apply (subst tendsto_norm_zero_iff[symmetric], rule filterlim_cong)
+      apply (simp_all add: eventually_at_filter field_simps nonzero_norm_divide)
+    done
+  then show ?thesis
+    by (simp add: has_field_derivative_def has_derivative_iff_norm bounded_linear_mult_right LIM_zero_iff)
+qed
 
 lemma DERIV_def: "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D"
   unfolding field_has_derivative_at has_field_derivative_def has_field_derivative_iff ..
@@ -773,10 +762,8 @@
 lemma has_vector_derivative_add_const:
   "((\<lambda>t. g t + z) has_vector_derivative f') net = ((\<lambda>t. g t) has_vector_derivative f') net"
   apply (intro iffI)
-   apply (drule has_vector_derivative_diff [where g = "\<lambda>t. z", OF _ has_vector_derivative_const])
-   apply simp
-  apply (drule has_vector_derivative_add [OF _ has_vector_derivative_const])
-  apply simp
+   apply (force dest: has_vector_derivative_diff [where g = "\<lambda>t. z", OF _ has_vector_derivative_const])
+  apply (force dest: has_vector_derivative_add [OF _ has_vector_derivative_const])
   done
 
 lemma has_vector_derivative_diff_const:
@@ -1027,22 +1014,27 @@
 
 lemma DERIV_LIM_iff:
   fixes f :: "'a::{real_normed_vector,inverse} \<Rightarrow> 'a"
-  shows "((\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0\<rightarrow> D) = ((\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D)"
-  apply (rule iffI)
-   apply (drule_tac k="- a" in LIM_offset)
-   apply simp
-  apply (drule_tac k="a" in LIM_offset)
-  apply (simp add: add.commute)
-  done
-
-lemmas DERIV_iff2 = has_field_derivative_iff
+  shows "((\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0\<rightarrow> D) = ((\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D)" (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then have "(\<lambda>x. (f (a + (x + - a)) - f a) / (x + - a)) \<midarrow>0 - - a\<rightarrow> D"
+    by (rule LIM_offset)
+  then show ?rhs
+    by simp
+next
+  assume ?rhs
+  then have "(\<lambda>x. (f (x+a) - f a) / ((x+a) - a)) \<midarrow>a-a\<rightarrow> D"
+    by (rule LIM_offset)
+  then show ?lhs
+    by (simp add: add.commute)
+qed
 
 lemma has_field_derivative_cong_ev:
   assumes "x = y"
     and *: "eventually (\<lambda>x. x \<in> s \<longrightarrow> f x = g x) (nhds x)"
     and "u = v" "s = t" "x \<in> s"
   shows "(f has_field_derivative u) (at x within s) = (g has_field_derivative v) (at y within t)"
-  unfolding DERIV_iff2
+  unfolding has_field_derivative_iff
 proof (rule filterlim_cong)
   from assms have "f y = g y"
     by (auto simp: eventually_nhds)
@@ -1054,7 +1046,7 @@
 lemma has_field_derivative_cong_eventually:
   assumes "eventually (\<lambda>x. f x = g x) (at x within s)" "f x=g x"
   shows "(f has_field_derivative u) (at x within s) = (g has_field_derivative u) (at x within s)"
-  unfolding DERIV_iff2
+  unfolding has_field_derivative_iff
   apply (rule tendsto_cong)
   apply (insert assms)
   by (auto elim: eventually_mono)
@@ -1698,7 +1690,7 @@
     and inj: "\<And>y. \<lbrakk>a < y; y < b\<rbrakk> \<Longrightarrow> f (g y) = y"
     and cont: "isCont g x"
   shows "DERIV g x :> inverse D"
-unfolding DERIV_iff2
+unfolding has_field_derivative_iff
 proof (rule LIM_equal2)
   show "0 < min (x - a) (b - x)"
     using x by arith
@@ -1711,7 +1703,7 @@
     by (simp add: inj)
 next
   have "(\<lambda>z. (f z - f (g x)) / (z - g x)) \<midarrow>g x\<rightarrow> D"
-    by (rule der [unfolded DERIV_iff2])
+    by (rule der [unfolded has_field_derivative_iff])
   then have 1: "(\<lambda>z. (f z - x) / (z - g x)) \<midarrow>g x\<rightarrow> D"
     using inj x by simp
   have 2: "\<exists>d>0. \<forall>y. y \<noteq> x \<and> norm (y - x) < d \<longrightarrow> g y \<noteq> g x"
diff -r ae4373f3d8d3 -r db0980691ef4 src/HOL/Number_Theory/Quadratic_Reciprocity.thy
--- a/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Sun Jul 15 10:41:57 2018 +0100
+++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Sun Jul 15 13:15:31 2018 +0100
@@ -370,7 +370,7 @@
     moreover from x have "(int p - 1) div 2 \<le> - 1 + x mod p"
       by (auto simp: BuDuF_def)
     moreover have "int p * (int q - 1) div 2 = int p * ((int q - 1) div 2)"
-      using div_mult1_eq odd_q by auto
+      by (subst div_mult1_eq) (simp add: odd_q)
     then have "p * (int q - 1) div 2 = p * ((int q + 1) div 2 - 1)"
       by fastforce
     ultimately have "x \<le> p * ((int q + 1) div 2 - 1) - 1 + x mod p"
diff -r ae4373f3d8d3 -r db0980691ef4 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sun Jul 15 10:41:57 2018 +0100
+++ b/src/HOL/Transcendental.thy	Sun Jul 15 13:15:31 2018 +0100
@@ -2303,7 +2303,7 @@
   have "((\<lambda>z::'a. exp(z) - 1) has_field_derivative 1) (at 0)"
     by (intro derivative_eq_intros | simp)+
   then show ?thesis
-    by (simp add: Deriv.DERIV_iff2)
+    by (simp add: Deriv.has_field_derivative_iff)
 qed
 
 lemma ln_at_0: "LIM x at_right 0. ln (x::real) :> at_bot"
diff -r ae4373f3d8d3 -r db0980691ef4 src/HOL/ex/Gauge_Integration.thy
--- a/src/HOL/ex/Gauge_Integration.thy	Sun Jul 15 10:41:57 2018 +0100
+++ b/src/HOL/ex/Gauge_Integration.thy	Sun Jul 15 13:15:31 2018 +0100
@@ -540,7 +540,7 @@
     fix x :: real assume "a \<le> x" and "x \<le> b"
     with f' have "DERIV f x :> f'(x)" by simp
     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)
+      by (simp add: has_field_derivative_iff LIM_eq)
     with \<open>0 < e\<close> obtain 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)