diff -r ec8c7c9459e0 -r 87d1bff264df src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sun Jul 15 18:22:31 2018 +0100
+++ b/src/HOL/Transcendental.thy	Sun Jul 15 21:58:50 2018 +0100
@@ -2236,7 +2236,7 @@
     assume "1 < x"
     from dense[OF this] obtain a where "1 < a" "a < x" by blast
     from \<open>a < x\<close> have "?l x < ?l a"
-    proof (rule DERIV_neg_imp_decreasing, safe)
+    proof (rule DERIV_neg_imp_decreasing)
       fix y
       assume "a \<le> y" "y \<le> x"
       with \<open>1 < a\<close> have "1 / y - 1 < 0" "0 < y"
@@ -2367,10 +2367,8 @@
   shows "x \<le> (exp x - inverse(exp x)) / 2"
 proof -
   have *: "exp a - inverse(exp a) - 2*a \<le> exp b - inverse(exp b) - 2*b" if "a \<le> b" for a b::real
-    apply (rule DERIV_nonneg_imp_nondecreasing [OF that])
     using exp_plus_inverse_exp
-    apply (intro exI allI impI conjI derivative_eq_intros | force)+
-    done
+    by (fastforce intro: derivative_eq_intros DERIV_nonneg_imp_nondecreasing [OF that])
   show ?thesis
     using*[OF assms] by simp
 qed
@@ -2559,9 +2557,7 @@
   by (simp add: log_def)
 
 lemma log_inverse: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> log a (inverse x) = - log a x"
-  apply (rule add_left_cancel [THEN iffD1, where a1 = "log a x"])
-  apply (simp add: log_mult [symmetric])
-  done
+  using ln_inverse log_def by auto
 
 lemma log_divide: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> log a (x/y) = log a x - log a y"
   by (simp add: log_mult divide_inverse log_inverse)
@@ -3134,10 +3130,7 @@
     show "eventually (\<lambda>xa. exp (ln (1 + x * xa) / xa) = (1 + x * xa) powr (1 / xa)) (at_right 0)"
       unfolding eventually_at_right[OF zero_less_one]
       using False
-      apply (intro exI[of _ "1 / \<bar>x\<bar>"])
-      apply (auto simp: field_simps powr_def abs_if)
-      apply (metis add_less_same_cancel1 mult_less_0_iff not_less_iff_gr_or_eq zero_less_one)
-      done
+      by (intro exI[of _ "1 / \<bar>x\<bar>"]) (auto simp: field_simps powr_def abs_if add_nonneg_eq_0_iff)
   qed (simp_all add: at_eq_sup_left_right)
 qed
 
@@ -5758,9 +5751,9 @@
         qed
         then have DERIV_in_rball: "\<forall>y. a \<le> y \<and> y \<le> b \<longrightarrow> DERIV (\<lambda>x. suminf (?c x) - arctan x) y :> 0"
           using \<open>-r < a\<close> \<open>b < r\<close> by auto
-        then show "\<forall>y. a < y \<and> y < b \<longrightarrow> DERIV (\<lambda>x. suminf (?c x) - arctan x) y :> 0"
+        then show "\<And>y. \<lbrakk>a < y; y < b\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. suminf (?c x) - arctan x) y :> 0"
           using \<open>\<bar>x\<bar> < r\<close> by auto
-        show "\<forall>y. a \<le> y \<and> y \<le> b \<longrightarrow> isCont (\<lambda>x. suminf (?c x) - arctan x) y"
+        show "\<And>y. \<lbrakk>a \<le> y; y \<le> b\<rbrakk> \<Longrightarrow>  isCont (\<lambda>x. suminf (?c x) - arctan x) y"
           using DERIV_in_rball DERIV_isCont by auto
       qed
     qed