1.1 --- a/src/HOL/Hyperreal/HyperPow.ML	Mon Dec 31 14:13:07 2001 +0100
     1.2 +++ b/src/HOL/Hyperreal/HyperPow.ML	Wed Jan 02 16:06:31 2002 +0100
     1.3 @@ -207,6 +207,22 @@
     1.4                 hypreal_of_nat_zero, hypreal_of_nat_Suc]) 1);
     1.5  qed "hrealpow_sum_square_expand";
     1.6  
     1.7 +
     1.8 +(*** Literal arithmetic involving powers, type hypreal ***)
     1.9 +
    1.10 +Goal "hypreal_of_real (x ^ n) = hypreal_of_real x ^ n";
    1.11 +by (induct_tac "n" 1); 
    1.12 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [nat_mult_distrib])));
    1.13 +qed "hypreal_of_real_power";
    1.14 +Addsimps [hypreal_of_real_power];
    1.15 +
    1.16 +Goal "(number_of v :: hypreal) ^ n = hypreal_of_real ((number_of v) ^ n)";
    1.17 +by (simp_tac (HOL_ss addsimps [hypreal_number_of_def, 
    1.18 +                               hypreal_of_real_power]) 1);
    1.19 +qed "power_hypreal_of_real_number_of";
    1.20 +
    1.21 +Addsimps [inst "n" "number_of ?w" power_hypreal_of_real_number_of];
    1.22 +
    1.23  (*---------------------------------------------------------------
    1.24     we'll prove the following theorem by going down to the
    1.25     level of the ultrafilter and relying on the analogous
    1.26 @@ -465,9 +481,9 @@
    1.27  by (auto_tac (claset(), simpset() addsimps [hyperpow]));
    1.28  qed "hyperpow_realpow";
    1.29  
    1.30 -Goalw [SReal_def]
    1.31 -     "(hypreal_of_real r) pow (hypnat_of_nat n) : Reals";
    1.32 -by (auto_tac (claset(), simpset() addsimps [hyperpow_realpow]));
    1.33 +Goalw [SReal_def] "(hypreal_of_real r) pow (hypnat_of_nat n) : Reals";
    1.34 +by (simp_tac (simpset() delsimps [hypreal_of_real_power]
    1.35 +			addsimps [hyperpow_realpow]) 1); 
    1.36  qed "hyperpow_SReal";
    1.37  Addsimps [hyperpow_SReal];
    1.38