diff -r 9963bb965a0e -r 4bc4b5c0ccfc src/HOL/NthRoot.thy
--- a/src/HOL/NthRoot.thy	Tue Jul 10 09:52:22 2018 +0100
+++ b/src/HOL/NthRoot.thy	Tue Jul 10 23:18:08 2018 +0100
@@ -314,34 +314,28 @@
     using x .
   show "x < x + 1"
     by simp
-  show "\<forall>y. 0 < y \<and> y < x + 1 \<longrightarrow> root n y ^ n = y"
-    using n by simp
   show "DERIV (\<lambda>x. x ^ n) (root n x) :> real n * root n x ^ (n - Suc 0)"
     by (rule DERIV_pow)
   show "real n * root n x ^ (n - Suc 0) \<noteq> 0"
     using n x by simp
   show "isCont (root n) x"
     by (rule isCont_real_root)
-qed
+qed (use n in auto)
 
 lemma DERIV_odd_real_root:
   assumes n: "odd n"
     and x: "x \<noteq> 0"
   shows "DERIV (root n) x :> inverse (real n * root n x ^ (n - Suc 0))"
 proof (rule DERIV_inverse_function)
-  show "x - 1 < x"
-    by simp
-  show "x < x + 1"
-    by simp
-  show "\<forall>y. x - 1 < y \<and> y < x + 1 \<longrightarrow> root n y ^ n = y"
-    using n by (simp add: odd_real_root_pow)
+  show "x - 1 < x" "x < x + 1"
+    by auto
   show "DERIV (\<lambda>x. x ^ n) (root n x) :> real n * root n x ^ (n - Suc 0)"
     by (rule DERIV_pow)
   show "real n * root n x ^ (n - Suc 0) \<noteq> 0"
     using odd_pos [OF n] x by simp
   show "isCont (root n) x"
     by (rule isCont_real_root)
-qed
+qed (use n odd_real_root_pow in auto)
 
 lemma DERIV_even_real_root:
   assumes n: "0 < n"
@@ -353,10 +347,10 @@
     by simp
   show "x < 0"
     using x .
-  show "\<forall>y. x - 1 < y \<and> y < 0 \<longrightarrow> - (root n y ^ n) = y"
-  proof (rule allI, rule impI, erule conjE)
-    fix y assume "x - 1 < y" and "y < 0"
-    then have "root n (-y) ^ n = -y" using \<open>0 < n\<close> by simp
+  show "- (root n y ^ n) = y" if "x - 1 < y" and "y < 0" for y
+  proof -
+    have "root n (-y) ^ n = -y" 
+      using that \<open>0 < n\<close> by simp
     with real_root_minus and \<open>even n\<close>
     show "- (root n y ^ n) = y" by simp
   qed
@@ -816,8 +810,6 @@
 lemmas real_root_pos2 = real_root_power_cancel
 lemmas real_root_pos_pos = real_root_gt_zero [THEN order_less_imp_le]
 lemmas real_root_pos_pos_le = real_root_ge_zero
-lemmas real_sqrt_mult_distrib = real_sqrt_mult
-lemmas real_sqrt_mult_distrib2 = real_sqrt_mult
 lemmas real_sqrt_eq_zero_cancel_iff = real_sqrt_eq_0_iff
 
 end