src/HOL/NthRoot.thy
changeset 60867 86e7560e07d0
parent 60758 d8d85a8172b5
child 61609 77b453bd616f
--- a/src/HOL/NthRoot.thy	Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/NthRoot.thy	Thu Aug 06 23:56:48 2015 +0200
@@ -112,7 +112,7 @@
   have x: "\<And>a b :: real. (0 < b \<and> a < 0) \<Longrightarrow> \<not> a > b" by auto
   fix a b :: real assume "0 < n" "sgn a * \<bar>a\<bar> ^ n < sgn b * \<bar>b\<bar> ^ n" then show "a < b"
     using power_less_imp_less_base[of a n b]  power_less_imp_less_base[of "-b" n "-a"]
-    by (simp add: sgn_real_def power_less_zero_eq x[of "a ^ n" "- ((- b) ^ n)"] split: split_if_asm)
+    by (simp add: sgn_real_def x [of "a ^ n" "- ((- b) ^ n)"] split: split_if_asm)
 qed
 
 lemma real_root_gt_zero: "\<lbrakk>0 < n; 0 < x\<rbrakk> \<Longrightarrow> 0 < root n x"
@@ -130,7 +130,7 @@
 by (auto simp add: order_le_less real_root_pow_pos)
 
 lemma sgn_root: "0 < n \<Longrightarrow> sgn (root n x) = sgn x"
-  by (auto split: split_root simp: sgn_real_def power_less_zero_eq)
+  by (auto split: split_root simp: sgn_real_def)
 
 lemma odd_real_root_pow: "odd n \<Longrightarrow> root n x ^ n = x"
   using sgn_power_root[of n x] by (simp add: odd_pos sgn_real_def split: split_if_asm)
@@ -496,7 +496,7 @@
 done
 
 lemma real_inv_sqrt_pow2: "0 < x ==> (inverse (sqrt x))\<^sup>2 = inverse x"
-by (simp add: power_inverse [symmetric])
+by (simp add: power_inverse)
 
 lemma real_sqrt_eq_zero_cancel: "[| 0 \<le> x; sqrt(x) = 0|] ==> x = 0"
 by simp
@@ -525,7 +525,7 @@
   apply (cases "x = 0")
   apply simp_all
   using sqrt_divide_self_eq[of x]
-  apply (simp add: inverse_eq_divide field_simps)
+  apply (simp add: field_simps)
   done
 
 lemma real_divide_square_eq [simp]: "(((r::real) * a) / (r * r)) = a / r"