src/HOL/Real/RealPow.ML
changeset 10043 a0364652e115
parent 9428 c8eb573114de
child 10606 e3229a37d53f
     1.1 --- a/src/HOL/Real/RealPow.ML	Thu Sep 21 10:42:49 2000 +0200
     1.2 +++ b/src/HOL/Real/RealPow.ML	Thu Sep 21 12:11:38 2000 +0200
     1.3 @@ -107,6 +107,11 @@
     1.4  qed "abs_realpow_minus_one";
     1.5  Addsimps [abs_realpow_minus_one];
     1.6  
     1.7 +Goal "abs((#-1) ^ n) = (#1::real)";
     1.8 +by (rtac (simplify (simpset()) abs_realpow_minus_one) 1);
     1.9 +qed "abs_realpow_minus_one2";
    1.10 +Addsimps [abs_realpow_minus_one2];
    1.11 +
    1.12  Goal "((r::real) * s) ^ n = (r ^ n) * (s ^ n)";
    1.13  by (induct_tac "n" 1);
    1.14  by (auto_tac (claset(),simpset() addsimps real_mult_ac));