src/HOL/NthRoot.thy
changeset 53076 47c9aff07725
parent 53015 a1119cf551e8
child 53594 8a9fb53294f4
     1.1 --- a/src/HOL/NthRoot.thy	Sun Aug 18 17:00:10 2013 +0200
     1.2 +++ b/src/HOL/NthRoot.thy	Sun Aug 18 18:49:45 2013 +0200
     1.3 @@ -464,7 +464,7 @@
     1.4  apply (rule real_sqrt_abs)
     1.5  done
     1.6  
     1.7 -lemma real_inv_sqrt_pow2: "0 < x ==> inverse (sqrt(x)) ^ 2 = inverse x"
     1.8 +lemma real_inv_sqrt_pow2: "0 < x ==> (inverse (sqrt x))\<^sup>2 = inverse x"
     1.9  by (simp add: power_inverse [symmetric])
    1.10  
    1.11  lemma real_sqrt_eq_zero_cancel: "[| 0 \<le> x; sqrt(x) = 0|] ==> x = 0"
    1.12 @@ -516,7 +516,7 @@
    1.13    by (simp add: zero_le_mult_iff)
    1.14  
    1.15  lemma real_sqrt_sum_squares_mult_squared_eq [simp]:
    1.16 -     "sqrt ((x\<^sup>2 + y\<^sup>2) * (xa\<^sup>2 + ya\<^sup>2)) ^ 2 = (x\<^sup>2 + y\<^sup>2) * (xa\<^sup>2 + ya\<^sup>2)"
    1.17 +     "(sqrt ((x\<^sup>2 + y\<^sup>2) * (xa\<^sup>2 + ya\<^sup>2)))\<^sup>2 = (x\<^sup>2 + y\<^sup>2) * (xa\<^sup>2 + ya\<^sup>2)"
    1.18    by (simp add: zero_le_mult_iff)
    1.19  
    1.20  lemma real_sqrt_sum_squares_eq_cancel: "sqrt (x\<^sup>2 + y\<^sup>2) = x \<Longrightarrow> y = 0"