src/HOL/Real/RealPow.thy
changeset 15251 bb6f072c8d10
parent 15229 1eb23f805c06
child 19279 48b527d0331b
     1.1 --- a/src/HOL/Real/RealPow.thy	Mon Oct 18 13:40:45 2004 +0200
     1.2 +++ b/src/HOL/Real/RealPow.thy	Tue Oct 19 18:18:45 2004 +0200
     1.3 @@ -57,7 +57,7 @@
     1.4  by (insert power_increasing [of 0 n "2::real"], simp)
     1.5  
     1.6  lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n"
     1.7 -apply (induct_tac "n")
     1.8 +apply (induct "n")
     1.9  apply (auto simp add: real_of_nat_Suc)
    1.10  apply (subst mult_2)
    1.11  apply (rule real_add_less_le_mono)
    1.12 @@ -97,12 +97,12 @@
    1.13  done
    1.14  
    1.15  lemma realpow_real_of_nat: "real (m::nat) ^ n = real (m ^ n)"
    1.16 -apply (induct_tac "n")
    1.17 +apply (induct "n")
    1.18  apply (auto simp add: real_of_nat_one real_of_nat_mult)
    1.19  done
    1.20  
    1.21  lemma realpow_real_of_nat_two_pos [simp] : "0 < real (Suc (Suc 0) ^ n)"
    1.22 -apply (induct_tac "n")
    1.23 +apply (induct "n")
    1.24  apply (auto simp add: real_of_nat_mult zero_less_mult_iff)
    1.25  done
    1.26  
    1.27 @@ -113,12 +113,12 @@
    1.28  
    1.29  lemma zero_less_realpow_abs_iff [simp]:
    1.30       "(0 < (abs x)^n) = (x \<noteq> (0::real) | n=0)" 
    1.31 -apply (induct_tac "n")
    1.32 +apply (induct "n")
    1.33  apply (auto simp add: zero_less_mult_iff)
    1.34  done
    1.35  
    1.36  lemma zero_le_realpow_abs [simp]: "(0::real) \<le> (abs x)^n"
    1.37 -apply (induct_tac "n")
    1.38 +apply (induct "n")
    1.39  apply (auto simp add: zero_le_mult_iff)
    1.40  done
    1.41  
    1.42 @@ -126,7 +126,7 @@
    1.43  subsection{*Literal Arithmetic Involving Powers, Type @{typ real}*}
    1.44  
    1.45  lemma real_of_int_power: "real (x::int) ^ n = real (x ^ n)"
    1.46 -apply (induct_tac "n")
    1.47 +apply (induct "n")
    1.48  apply (simp_all add: nat_mult_distrib)
    1.49  done
    1.50  declare real_of_int_power [symmetric, simp]
    1.51 @@ -235,7 +235,7 @@
    1.52  by (case_tac "n", auto)
    1.53  
    1.54  lemma real_num_zero_less_two_pow [simp]: "0 < (2::real) ^ (4*d)"
    1.55 -apply (induct_tac "d")
    1.56 +apply (induct "d")
    1.57  apply (auto simp add: realpow_num_eq_if)
    1.58  done
    1.59