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"