src/HOL/RealVector.thy
changeset 30273 ecd6f0ca62ea
parent 30242 aea5d7fa7ef5
child 30729 461ee3e49ad3
     1.1 --- a/src/HOL/RealVector.thy	Thu Mar 05 00:16:28 2009 +0100
     1.2 +++ b/src/HOL/RealVector.thy	Wed Mar 04 17:12:23 2009 -0800
     1.3 @@ -260,7 +260,7 @@
     1.4  
     1.5  lemma of_real_power [simp]:
     1.6    "of_real (x ^ n) = (of_real x :: 'a::{real_algebra_1,recpower}) ^ n"
     1.7 -by (induct n) (simp_all add: power_Suc)
     1.8 +by (induct n) simp_all
     1.9  
    1.10  lemma of_real_eq_iff [simp]: "(of_real x = of_real y) = (x = y)"
    1.11  by (simp add: of_real_def scaleR_cancel_right)
    1.12 @@ -624,13 +624,13 @@
    1.13    also from Suc have "\<dots> \<le> norm x * norm x ^ n"
    1.14      using norm_ge_zero by (rule mult_left_mono)
    1.15    finally show "norm (x ^ Suc n) \<le> norm x ^ Suc n"
    1.16 -    by (simp add: power_Suc)
    1.17 +    by simp
    1.18  qed
    1.19  
    1.20  lemma norm_power:
    1.21    fixes x :: "'a::{real_normed_div_algebra,recpower}"
    1.22    shows "norm (x ^ n) = norm x ^ n"
    1.23 -by (induct n) (simp_all add: power_Suc norm_mult)
    1.24 +by (induct n) (simp_all add: norm_mult)
    1.25  
    1.26  
    1.27  subsection {* Sign function *}