starting to get rid of sumr
authornipkow
Fri Feb 18 11:48:53 2005 +0100 (2005-02-18)
changeset 155363ce1cb7a24f0
parent 15535 a0cf3a19ee36
child 15537 5538d3244b4d
starting to get rid of sumr
src/HOL/Hyperreal/HSeries.thy
src/HOL/Hyperreal/Integration.thy
src/HOL/Hyperreal/MacLaurin.thy
src/HOL/Hyperreal/Series.thy
src/HOL/Hyperreal/Transcendental.thy
src/HOL/Real/Real.thy
     1.1 --- a/src/HOL/Hyperreal/HSeries.thy	Fri Feb 18 11:48:42 2005 +0100
     1.2 +++ b/src/HOL/Hyperreal/HSeries.thy	Fri Feb 18 11:48:53 2005 +0100
     1.3 @@ -73,12 +73,12 @@
     1.4  
     1.5  lemma sumhr_add: "sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)"
     1.6  apply (cases m, cases n)
     1.7 -apply (simp add: sumhr hypreal_add sumr_add)
     1.8 +apply (simp add: sumhr hypreal_add setsum_addf)
     1.9  done
    1.10  
    1.11  lemma sumhr_mult: "hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)"
    1.12  apply (cases m, cases n)
    1.13 -apply (simp add: sumhr hypreal_of_real_def hypreal_mult sumr_mult)
    1.14 +apply (simp add: sumhr hypreal_of_real_def hypreal_mult setsum_mult)
    1.15  done
    1.16  
    1.17  lemma sumhr_split_add: "n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)"
    1.18 @@ -92,7 +92,7 @@
    1.19  
    1.20  lemma sumhr_hrabs: "abs(sumhr(m,n,f)) \<le> sumhr(m,n,%i. abs(f i))"
    1.21  apply (cases n, cases m)
    1.22 -apply (simp add: sumhr hypreal_le hypreal_hrabs sumr_rabs)
    1.23 +apply (simp add: sumhr hypreal_le hypreal_hrabs setsum_abs)
    1.24  done
    1.25  
    1.26  text{* other general version also needed *}
    1.27 @@ -100,9 +100,8 @@
    1.28     "(\<forall>r. m \<le> r & r < n --> f r = g r) -->  
    1.29        sumhr(hypnat_of_nat m, hypnat_of_nat n, f) =  
    1.30        sumhr(hypnat_of_nat m, hypnat_of_nat n, g)"
    1.31 -apply (safe, drule sumr_fun_eq)
    1.32 -apply (simp add: sumhr hypnat_of_nat_eq)
    1.33 -done
    1.34 +by (fastsimp simp add: sumhr hypnat_of_nat_eq intro:setsum_cong)
    1.35 +
    1.36  
    1.37  lemma sumhr_const:
    1.38       "sumhr(0, n, %i. r) = hypreal_of_hypnat n * hypreal_of_real r"
    1.39 @@ -119,7 +118,7 @@
    1.40  
    1.41  lemma sumhr_minus: "sumhr(m, n, %i. - f i) = - sumhr(m, n, f)"
    1.42  apply (cases m, cases n)
    1.43 -apply (simp add: sumhr hypreal_minus sumr_minus)
    1.44 +apply (simp add: sumhr hypreal_minus setsum_negf)
    1.45  done
    1.46  
    1.47  lemma sumhr_shift_bounds:
     2.1 --- a/src/HOL/Hyperreal/Integration.thy	Fri Feb 18 11:48:42 2005 +0100
     2.2 +++ b/src/HOL/Hyperreal/Integration.thy	Fri Feb 18 11:48:53 2005 +0100
     2.3 @@ -343,7 +343,7 @@
     2.4  lemma Integral_mult_const: "a \<le> b ==> Integral(a,b) (%x. c)  (c*(b - a))"
     2.5  apply (auto simp add: order_le_less rsum_def Integral_def)
     2.6  apply (rule_tac x = "%x. b - a" in exI)
     2.7 -apply (auto simp add: sumr_mult [symmetric] gauge_def abs_interval_iff 
     2.8 +apply (auto simp add: setsum_mult [symmetric] gauge_def abs_interval_iff 
     2.9                 right_diff_distrib [symmetric] partition tpart_def)
    2.10  done
    2.11  
    2.12 @@ -351,7 +351,7 @@
    2.13       "[| a \<le> b; Integral(a,b) f k |] ==> Integral(a,b) (%x. c * f x) (c * k)"
    2.14  apply (auto simp add: order_le_less 
    2.15              dest: Integral_unique [OF order_refl Integral_zero])
    2.16 -apply (auto simp add: rsum_def Integral_def sumr_mult [symmetric] mult_assoc)
    2.17 +apply (auto simp add: rsum_def Integral_def setsum_mult[symmetric] mult_assoc)
    2.18  apply (rule_tac a2 = c in abs_ge_zero [THEN real_le_imp_less_or_eq, THEN disjE])
    2.19   prefer 2 apply force
    2.20  apply (drule_tac x = "e/abs c" in spec, auto)
    2.21 @@ -459,13 +459,13 @@
    2.22          in sumr_partition_eq_diff_bounds)
    2.23   apply (simp add: partition_lhs partition_rhs)
    2.24  apply (drule sym, simp)
    2.25 -apply (simp (no_asm) add: sumr_diff)
    2.26 -apply (rule sumr_rabs [THEN order_trans])
    2.27 +apply (simp (no_asm) add: setsum_subtractf[symmetric])
    2.28 +apply (rule setsum_abs [THEN order_trans])
    2.29  apply (subgoal_tac "ea = sumr 0 (psize D) (%n. (ea / (b - a)) * (D (Suc n) - (D n)))")
    2.30  apply (simp add: abs_minus_commute)
    2.31  apply (rule_tac t = ea in ssubst, assumption)
    2.32  apply (rule sumr_le2)
    2.33 -apply (rule_tac [2] sumr_mult [THEN subst])
    2.34 +apply (rule_tac [2] setsum_mult [THEN subst])
    2.35  apply (auto simp add: partition_rhs partition_lhs partition_lb partition_ub
    2.36            fine_def)
    2.37  done
    2.38 @@ -769,7 +769,7 @@
    2.39  done
    2.40  
    2.41  lemma rsum_add: "rsum (D, p) (%x. f x + g x) =  rsum (D, p) f + rsum(D, p) g"
    2.42 -by (simp add: rsum_def sumr_add left_distrib)
    2.43 +by (simp add: rsum_def setsum_addf left_distrib)
    2.44  
    2.45  text{* Bartle/Sherbert: Theorem 10.1.5 p. 278 *}
    2.46  lemma Integral_add_fun:
     3.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Fri Feb 18 11:48:42 2005 +0100
     3.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Fri Feb 18 11:48:53 2005 +0100
     3.3 @@ -267,7 +267,7 @@
     3.4  apply (rule_tac x = "-t" in exI, auto)
     3.5  apply (subgoal_tac "(\<Sum>m = 0..<n. -1 ^ m * diff m 0 * (-h)^m / real(fact m)) =
     3.6                      (\<Sum>m = 0..<n. diff m 0 * h ^ m / real(fact m))")
     3.7 -apply (rule_tac [2] sumr_fun_eq)
     3.8 +apply (rule_tac [2] setsum_cong[OF refl])
     3.9  apply (auto simp add: divide_inverse power_mult_distrib [symmetric])
    3.10  done
    3.11  
    3.12 @@ -435,7 +435,7 @@
    3.13  apply (drule_tac x = x in spec, simp)
    3.14  apply (erule ssubst)
    3.15  apply (rule_tac x = t in exI, simp)
    3.16 -apply (rule sumr_fun_eq)
    3.17 +apply (rule setsum_cong[OF refl])
    3.18  apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
    3.19  done
    3.20  
    3.21 @@ -465,7 +465,7 @@
    3.22  apply (simp (no_asm) add: times_divide_eq)
    3.23  apply (erule ssubst)
    3.24  apply (rule_tac x = t in exI, simp)
    3.25 -apply (rule sumr_fun_eq)
    3.26 +apply (rule setsum_cong[OF refl])
    3.27  apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
    3.28  done
    3.29  
    3.30 @@ -483,7 +483,7 @@
    3.31  apply (simp (no_asm) add: times_divide_eq)
    3.32  apply (erule ssubst)
    3.33  apply (rule_tac x = t in exI, simp)
    3.34 -apply (rule sumr_fun_eq)
    3.35 +apply (rule setsum_cong[OF refl])
    3.36  apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
    3.37  done
    3.38  
    3.39 @@ -516,7 +516,7 @@
    3.40  apply (drule_tac x = x in spec, simp)
    3.41  apply (erule ssubst)
    3.42  apply (rule_tac x = t in exI, simp)
    3.43 -apply (rule sumr_fun_eq)
    3.44 +apply (rule setsum_cong[OF refl])
    3.45  apply (auto simp add: cos_zero_iff even_mult_two_ex)
    3.46  done
    3.47  
    3.48 @@ -535,7 +535,7 @@
    3.49  apply (simp (no_asm) add: times_divide_eq)
    3.50  apply (erule ssubst)
    3.51  apply (rule_tac x = t in exI, simp)
    3.52 -apply (rule sumr_fun_eq)
    3.53 +apply (rule setsum_cong[OF refl])
    3.54  apply (auto simp add: cos_zero_iff even_mult_two_ex)
    3.55  done
    3.56  
    3.57 @@ -554,7 +554,7 @@
    3.58  apply (simp (no_asm) add: times_divide_eq)
    3.59  apply (erule ssubst)
    3.60  apply (rule_tac x = t in exI, simp)
    3.61 -apply (rule sumr_fun_eq)
    3.62 +apply (rule setsum_cong[OF refl])
    3.63  apply (auto simp add: cos_zero_iff even_mult_two_ex)
    3.64  done
    3.65  
    3.66 @@ -585,10 +585,10 @@
    3.67      apply (rule lemma_DERIV_subst, rule DERIV_minus, rule DERIV_cos, simp)
    3.68      apply (erule ssubst)
    3.69      apply (rule sin_bound_lemma)
    3.70 -    apply (rule sumr_fun_eq, safe)
    3.71 -    apply (rule_tac f = "%u. u * (x^r)" in arg_cong)
    3.72 +    apply (rule setsum_cong[OF refl])
    3.73 +    apply (rule_tac f = "%u. u * (x^xa)" in arg_cong)
    3.74      apply (subst even_even_mod_4_iff)
    3.75 -    apply (cut_tac m=r in mod_exhaust_less_4, simp, safe)
    3.76 +    apply (cut_tac m=xa in mod_exhaust_less_4, simp, safe)
    3.77      apply (simp_all add:even_num_iff)
    3.78      apply (drule lemma_even_mod_4_div_2[simplified])
    3.79      apply(simp add: numeral_2_eq_2 divide_inverse)
     4.1 --- a/src/HOL/Hyperreal/Series.thy	Fri Feb 18 11:48:42 2005 +0100
     4.2 +++ b/src/HOL/Hyperreal/Series.thy	Fri Feb 18 11:48:53 2005 +0100
     4.3 @@ -11,13 +11,15 @@
     4.4  imports SEQ Lim
     4.5  begin
     4.6  
     4.7 +declare atLeastLessThan_empty[simp];
     4.8 +
     4.9  syntax sumr :: "[nat,nat,(nat=>real)] => real"
    4.10  translations
    4.11    "sumr m n f" => "setsum (f::nat=>real) (atLeastLessThan m n)"
    4.12  
    4.13  constdefs
    4.14     sums  :: "[nat=>real,real] => bool"     (infixr "sums" 80)
    4.15 -   "f sums s  == (%n. sumr 0 n f) ----> s"
    4.16 +   "f sums s  == (%n. setsum f {0..<n}) ----> s"
    4.17  
    4.18     summable :: "(nat=>real) => bool"
    4.19     "summable f == (\<exists>s. f sums s)"
    4.20 @@ -27,9 +29,10 @@
    4.21  
    4.22  
    4.23  lemma sumr_Suc [simp]:
    4.24 -     "sumr m (Suc n) f = (if n < m then 0 else sumr m n f + f(n))"
    4.25 -by (simp add: atLeastLessThanSuc)
    4.26 +  "setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))"
    4.27 +by (simp add: atLeastLessThanSuc add_commute)
    4.28  
    4.29 +(*
    4.30  lemma sumr_add: "sumr m n f + sumr m n g = sumr m n (%n. f n + g n)"
    4.31  by (simp add: setsum_addf)
    4.32  
    4.33 @@ -42,13 +45,22 @@
    4.34  apply (rename_tac k) 
    4.35  apply (subgoal_tac "n=k", auto) 
    4.36  done
    4.37 +*)
    4.38 +
    4.39 +lemma sumr_split_add: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
    4.40 +  setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}"
    4.41 +by (simp add:setsum_Un_disjoint[symmetric] ivl_disj_int ivl_disj_un)
    4.42  
    4.43  lemma sumr_split_add_minus:
    4.44       "n < p ==> sumr 0 p f + - sumr 0 n f = sumr n p (f::nat=>real)"
    4.45 -apply (drule_tac f1 = f in sumr_split_add [symmetric])
    4.46 +using sumr_split_add [of 0 n p f,symmetric]
    4.47  apply (simp add: add_ac)
    4.48  done
    4.49  
    4.50 +lemma sumr_diff_mult_const: "sumr 0 n f - (real n*r) = sumr 0 n (%i. f i - r)"
    4.51 +by (simp add: diff_minus setsum_addf real_of_nat_def)
    4.52 +
    4.53 +(*
    4.54  lemma sumr_rabs: "abs(sumr m n  (f::nat=>real)) \<le> sumr m n (%i. abs(f i))"
    4.55  by (simp add: setsum_abs)
    4.56  
    4.57 @@ -60,14 +72,12 @@
    4.58       "(\<forall>r. m \<le> r & r < n --> f r = g r) ==> sumr m n f = sumr m n g"
    4.59  by (auto intro: setsum_cong) 
    4.60  
    4.61 -lemma sumr_diff_mult_const: "sumr 0 n f - (real n*r) = sumr 0 n (%i. f i - r)"
    4.62 -by (simp add: diff_minus setsum_addf real_of_nat_def)
    4.63 -
    4.64  lemma sumr_less_bounds_zero [simp]: "n < m ==> sumr m n f = 0"
    4.65  by (simp add: atLeastLessThan_empty)
    4.66  
    4.67  lemma sumr_minus: "sumr m n (%i. - f i) = - sumr m n f"
    4.68  by (simp add: Finite_Set.setsum_negf)
    4.69 +*)
    4.70  
    4.71  lemma sumr_shift_bounds: "sumr (m+k) (n+k) f = sumr m n (%i. f(i + k))"
    4.72  by (induct "n", auto)
    4.73 @@ -114,6 +124,7 @@
    4.74  apply (drule_tac x = n in spec, arith)
    4.75  done
    4.76  
    4.77 +(* FIXME generalize *)
    4.78  lemma rabs_sumr_rabs_cancel [simp]:
    4.79       "abs (sumr m n (%k. abs (f k))) = (sumr m n (%k. abs (f k)))"
    4.80  by (induct "n", simp_all add: add_increasing)
    4.81 @@ -132,10 +143,10 @@
    4.82  apply (induct "n")
    4.83  apply (case_tac [2] "n", auto)
    4.84  done
    4.85 -
    4.86 +(*
    4.87  lemma sumr_diff: "sumr m n f - sumr m n g = sumr m n (%n. f n - g n)"
    4.88 -by (simp add: diff_minus sumr_add [symmetric] sumr_minus)
    4.89 -
    4.90 +by (simp add: diff_minus setsum_addf setsum_negf)
    4.91 +*)
    4.92  lemma sumr_subst [rule_format (no_asm)]:
    4.93       "(\<forall>p. m \<le> p & p < m+n --> (f p = g p)) --> sumr m n f = sumr m n g"
    4.94  by (induct "n", auto)
    4.95 @@ -213,14 +224,14 @@
    4.96  done
    4.97  
    4.98  lemma sums_mult: "x sums x0 ==> (%n. c * x(n)) sums (c * x0)"
    4.99 -by (auto simp add: sums_def sumr_mult [symmetric]
   4.100 +by (auto simp add: sums_def setsum_mult [symmetric]
   4.101           intro!: LIMSEQ_mult intro: LIMSEQ_const)
   4.102  
   4.103  lemma sums_divide: "x sums x' ==> (%n. x(n)/c) sums (x'/c)"
   4.104  by (simp add: real_divide_def sums_mult mult_commute [of _ "inverse c"])
   4.105  
   4.106  lemma sums_diff: "[| x sums x0; y sums y0 |] ==> (%n. x n - y n) sums (x0-y0)"
   4.107 -by (auto simp add: sums_def sumr_diff [symmetric] intro: LIMSEQ_diff)
   4.108 +by (auto simp add: sums_def setsum_subtractf intro: LIMSEQ_diff)
   4.109  
   4.110  lemma suminf_mult: "summable f ==> suminf f * c = suminf(%n. f n * c)"
   4.111  by (auto intro!: sums_unique sums_mult summable_sums simp add: mult_commute)
   4.112 @@ -234,7 +245,7 @@
   4.113  by (auto intro!: sums_diff sums_unique summable_sums)
   4.114  
   4.115  lemma sums_minus: "x sums x0 ==> (%n. - x n) sums - x0"
   4.116 -by (auto simp add: sums_def intro!: LIMSEQ_minus simp add: sumr_minus)
   4.117 +by (auto simp add: sums_def intro!: LIMSEQ_minus simp add: setsum_negf)
   4.118  
   4.119  lemma sums_group:
   4.120       "[|summable f; 0 < k |] ==> (%n. sumr (n*k) (n*k + k) f) sums (suminf f)"
   4.121 @@ -356,7 +367,7 @@
   4.122  apply (drule_tac x = m in spec)
   4.123  apply (auto, rotate_tac 2, drule_tac x = n in spec)
   4.124  apply (rule_tac y = "sumr m n (%k. abs (f k))" in order_le_less_trans)
   4.125 -apply (rule sumr_rabs)
   4.126 +apply (rule setsum_abs)
   4.127  apply (rule_tac y = "sumr m n g" in order_le_less_trans)
   4.128  apply (auto intro: sumr_le2 simp add: abs_interval_iff)
   4.129  done
   4.130 @@ -387,18 +398,18 @@
   4.131  
   4.132  text{*Absolute convergence imples normal convergence*}
   4.133  lemma summable_rabs_cancel: "summable (%n. abs (f n)) ==> summable f"
   4.134 -apply (auto simp add: sumr_rabs summable_Cauchy)
   4.135 +apply (auto simp add: summable_Cauchy)
   4.136  apply (drule spec, auto)
   4.137  apply (rule_tac x = N in exI, auto)
   4.138  apply (drule spec, auto)
   4.139  apply (rule_tac y = "sumr m n (%n. abs (f n))" in order_le_less_trans)
   4.140 -apply (auto intro: sumr_rabs)
   4.141 +apply (auto)
   4.142  done
   4.143  
   4.144  text{*Absolute convergence of series*}
   4.145  lemma summable_rabs:
   4.146       "summable (%n. abs (f n)) ==> abs(suminf f) \<le> suminf (%n. abs(f n))"
   4.147 -by (auto intro: LIMSEQ_le LIMSEQ_imp_rabs summable_rabs_cancel summable_sumr_LIMSEQ_suminf sumr_rabs)
   4.148 +by (auto intro: LIMSEQ_le LIMSEQ_imp_rabs summable_rabs_cancel summable_sumr_LIMSEQ_suminf)
   4.149  
   4.150  
   4.151  subsection{* The Ratio Test*}
   4.152 @@ -465,19 +476,13 @@
   4.153  val summable_def = thm"summable_def";
   4.154  val suminf_def = thm"suminf_def";
   4.155  
   4.156 -val sumr_add = thm "sumr_add";
   4.157 -val sumr_mult = thm "sumr_mult";
   4.158  val sumr_split_add = thm "sumr_split_add";
   4.159 -val sumr_rabs = thm "sumr_rabs";
   4.160 -val sumr_fun_eq = thm "sumr_fun_eq";
   4.161 -val sumr_diff_mult_const = thm "sumr_diff_mult_const";
   4.162  val sumr_minus_one_realpow_zero = thm "sumr_minus_one_realpow_zero";
   4.163  val sumr_le2 = thm "sumr_le2";
   4.164  val rabs_sumr_rabs_cancel = thm "rabs_sumr_rabs_cancel";
   4.165  val sumr_zero = thm "sumr_zero";
   4.166  val Suc_le_imp_diff_ge2 = thm "Suc_le_imp_diff_ge2";
   4.167  val sumr_one_lb_realpow_zero = thm "sumr_one_lb_realpow_zero";
   4.168 -val sumr_diff = thm "sumr_diff";
   4.169  val sumr_subst = thm "sumr_subst";
   4.170  val sumr_bound = thm "sumr_bound";
   4.171  val sumr_bound2 = thm "sumr_bound2";
     5.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Fri Feb 18 11:48:42 2005 +0100
     5.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Fri Feb 18 11:48:53 2005 +0100
     5.3 @@ -366,7 +366,7 @@
     5.4  lemma lemma_realpow_diff_sumr:
     5.5       "sumr 0 (Suc n) (%p. (x ^ p) * y ^ ((Suc n) - p)) =  
     5.6        y * sumr 0 (Suc n) (%p. (x ^ p) * (y ^ (n - p)))"
     5.7 -apply (auto simp add: sumr_mult simp del: sumr_Suc)
     5.8 +apply (auto simp add: setsum_mult simp del: sumr_Suc)
     5.9  apply (rule sumr_subst)
    5.10  apply (intro strip)
    5.11  apply (subst lemma_realpow_diff)
    5.12 @@ -504,10 +504,10 @@
    5.13              simp del: realpow_Suc sumr_Suc)
    5.14  apply (auto simp add: lemma_realpow_rev_sumr simp del: sumr_Suc)
    5.15  apply (auto simp add: real_of_nat_Suc sumr_diff_mult_const left_distrib 
    5.16 -                sumdiff lemma_termdiff1 sumr_mult)
    5.17 +                sumdiff lemma_termdiff1 setsum_mult)
    5.18  apply (auto intro!: sumr_subst simp add: diff_minus real_add_assoc)
    5.19  apply (simp add: diff_minus [symmetric] less_iff_Suc_add) 
    5.20 -apply (auto simp add: sumr_mult lemma_realpow_diff_sumr2 mult_ac simp
    5.21 +apply (auto simp add: setsum_mult lemma_realpow_diff_sumr2 mult_ac simp
    5.22                   del: sumr_Suc realpow_Suc)
    5.23  done
    5.24  
    5.25 @@ -518,7 +518,7 @@
    5.26  apply (subst lemma_termdiff2, assumption)
    5.27  apply (simp add: abs_mult mult_commute) 
    5.28  apply (simp add: mult_commute [of _ "K ^ (n - 2)"]) 
    5.29 -apply (rule sumr_rabs [THEN real_le_trans])
    5.30 +apply (rule setsum_abs [THEN real_le_trans])
    5.31  apply (simp add: mult_assoc [symmetric])
    5.32  apply (simp add: mult_commute [of _ "real (n - Suc 0)"])
    5.33  apply (auto intro!: sumr_bound2 simp add: abs_mult)
    5.34 @@ -535,7 +535,7 @@
    5.35  apply (subgoal_tac [2] "0 \<le> K")
    5.36  apply (drule_tac [2] n = d in zero_le_power)
    5.37  apply (auto simp del: sumr_Suc)
    5.38 -apply (rule sumr_rabs [THEN real_le_trans])
    5.39 +apply (rule setsum_abs [THEN real_le_trans])
    5.40  apply (rule sumr_bound2, auto dest!: less_add_one intro!: mult_mono simp add: abs_mult power_add)
    5.41  apply (auto intro!: power_mono zero_le_power simp add: power_abs, arith+)
    5.42  done
     6.1 --- a/src/HOL/Real/Real.thy	Fri Feb 18 11:48:42 2005 +0100
     6.2 +++ b/src/HOL/Real/Real.thy	Fri Feb 18 11:48:53 2005 +0100
     6.3 @@ -1,2 +1,4 @@
     6.4 -
     6.5 -Real = RComplete + RealPow
     6.6 +theory Real
     6.7 +imports RComplete RealPow
     6.8 +begin
     6.9 +end
    6.10 \ No newline at end of file