# HG changeset patch
# User nipkow
# Date 1007056983 -3600
# Node ID c69bee072501c88221f45b56f810d33c76261e4a
# Parent  8743e8305611172d882a7bbff830398df7ba75c5
*** empty log message ***

diff -r 8743e8305611 -r c69bee072501 src/HOL/Hyperreal/HyperPow.ML
--- a/src/HOL/Hyperreal/HyperPow.ML	Thu Nov 29 17:39:23 2001 +0100
+++ b/src/HOL/Hyperreal/HyperPow.ML	Thu Nov 29 19:03:03 2001 +0100
@@ -283,7 +283,7 @@
 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
 by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
 by (auto_tac (claset(),
-              simpset() addsimps [hypreal_hrabs, hyperpow,realpow_abs]));
+              simpset() addsimps [hypreal_hrabs, hyperpow,realpow_abs RS sym]));
 qed "hyperpow_hrabs";
 
 Goal "r pow (n + m) = (r pow n) * (r pow m)";
diff -r 8743e8305611 -r c69bee072501 src/HOL/Hyperreal/MacLaurin.ML
--- a/src/HOL/Hyperreal/MacLaurin.ML	Thu Nov 29 17:39:23 2001 +0100
+++ b/src/HOL/Hyperreal/MacLaurin.ML	Thu Nov 29 19:03:03 2001 +0100
@@ -492,7 +492,8 @@
 by (dtac lemma_odd_mod_4_div_2 1);
 by (asm_full_simp_tac (simpset() addsimps [numeral_2_eq_2, real_divide_def]) 1);
 by (auto_tac (claset() addSIs [real_mult_le_lemma,real_mult_le_le_mono2],
-      simpset() addsimps [real_divide_def,abs_mult,abs_inverse,realpow_abs]));
+      simpset() addsimps [real_divide_def,abs_mult,abs_inverse,realpow_abs RS
+sym]));
 qed "Maclaurin_sin_bound";
 
 Goal "0 < n --> Suc (Suc (2 * n - 2)) = 2*n";
diff -r 8743e8305611 -r c69bee072501 src/HOL/Hyperreal/SEQ.ML
--- a/src/HOL/Hyperreal/SEQ.ML	Thu Nov 29 17:39:23 2001 +0100
+++ b/src/HOL/Hyperreal/SEQ.ML	Thu Nov 29 19:03:03 2001 +0100
@@ -1222,7 +1222,7 @@
 by (res_inst_tac [("x","1")] exI 1);
 by (auto_tac (claset() addDs [conjI RS realpow_le] 
                        addIs [order_less_imp_le], 
-              simpset() addsimps [abs_eqI1, realpow_abs RS sym] ));
+              simpset() addsimps [abs_eqI1, realpow_abs] ));
 qed "Bseq_realpow";
 
 Goal "[| 0 <= x; x < 1 |] ==> monoseq (%n. x ^ n)";
@@ -1287,7 +1287,7 @@
 Goal "abs(c) < 1 ==> (%n. c ^ n) ----> 0";
 by (rtac (LIMSEQ_rabs_zero RS iffD1) 1);
 by (auto_tac (claset() addIs [LIMSEQ_rabs_realpow_zero],
-              simpset() addsimps [realpow_abs RS sym]));
+              simpset() addsimps [realpow_abs]));
 qed "LIMSEQ_rabs_realpow_zero2";
 
 Goal "abs(c) < 1 ==> (%n. c ^ n) ----NS> 0";
diff -r 8743e8305611 -r c69bee072501 src/HOL/Hyperreal/Transcendental.ML
--- a/src/HOL/Hyperreal/Transcendental.ML	Thu Nov 29 17:39:23 2001 +0100
+++ b/src/HOL/Hyperreal/Transcendental.ML	Thu Nov 29 19:03:03 2001 +0100
@@ -315,7 +315,7 @@
     summable_comparison_test 1);
 by (rtac summable_exp 2);
 by (res_inst_tac [("x","0")] exI 1);
-by (auto_tac (claset(), simpset() addsimps [realpow_abs,
+by (auto_tac (claset(), simpset() addsimps [realpow_abs RS sym,
     abs_ge_zero,abs_mult,real_0_le_mult_iff]));
 by (auto_tac (claset() addIs [real_mult_le_le_mono2],
     simpset() addsimps [real_inverse_gt_0,abs_eqI2,abs_ge_zero]));
@@ -329,7 +329,7 @@
     summable_comparison_test 1);
 by (rtac summable_exp 2);
 by (res_inst_tac [("x","0")] exI 1);
-by (auto_tac (claset(), simpset() addsimps [realpow_abs,abs_ge_zero,abs_mult,
+by (auto_tac (claset(), simpset() addsimps [realpow_abs RS sym,abs_ge_zero,abs_mult,
     real_0_le_mult_iff]));
 by (auto_tac (claset() addSIs [real_mult_le_le_mono2],
     simpset() addsimps [real_inverse_gt_0,abs_eqI2,abs_ge_zero]));
@@ -453,27 +453,27 @@
 by (res_inst_tac [("z","abs (x ^ n)")] (CLAIM_SIMP 
     "[| (0::real) <z; x*z<=y*z |] ==> x<=y" [real_mult_le_cancel1]) 1);
 by (auto_tac (claset(),
-    simpset() addsimps [real_mult_assoc,realpow_abs RS sym]));
+    simpset() addsimps [real_mult_assoc,realpow_abs]));
 by (dres_inst_tac [("x","0")] spec 2 THEN Force_tac 2); 
 by (auto_tac (claset(),simpset() addsimps [abs_ge_zero,
-    abs_mult,realpow_abs RS sym] @ real_mult_ac));
+    abs_mult,realpow_abs] @ real_mult_ac));
 by (res_inst_tac [("x2","z ^ n")] (abs_ge_zero RS real_le_imp_less_or_eq
     RS disjE) 1 THEN dtac sym 2);
 by (auto_tac (claset() addSIs [real_mult_le_le_mono2],
     simpset() addsimps [real_mult_assoc RS sym,
-    realpow_abs RS sym,summable_def]));
+    realpow_abs,summable_def]));
 by (res_inst_tac [("x","K * inverse(1 - (abs(z) * inverse(abs x)))")] exI 1);
 by (auto_tac (claset() addSIs [sums_mult],simpset() addsimps [real_mult_assoc]));
 by (subgoal_tac 
     "abs(z ^ n) * inverse(abs x ^ n) = (abs(z) * inverse(abs x)) ^ n" 1);
-by (auto_tac (claset(),simpset() addsimps [realpow_abs]));
+by (auto_tac (claset(),simpset() addsimps [realpow_abs RS sym]));
 by (subgoal_tac "x ~= 0" 1);
 by (subgoal_tac "x ~= 0" 3);
 by (auto_tac (claset(),simpset() addsimps 
     [abs_inverse RS sym,realpow_not_zero,abs_mult 
      RS sym,realpow_inverse,realpow_mult RS sym]));
 by (auto_tac (claset() addSIs [geometric_sums],simpset() addsimps
-    [realpow_abs RS sym,real_divide_eq_inverse RS sym]));
+    [realpow_abs,real_divide_eq_inverse RS sym]));
 by (res_inst_tac [("z","abs(x)")] (CLAIM_SIMP 
     "[|(0::real)<z; x*z<y*z |] ==> x<y" [real_mult_less_cancel1]) 1);
 by (auto_tac (claset(),simpset() addsimps [abs_ge_zero,
@@ -484,7 +484,7 @@
 \     ==> summable (%n. f(n) * (z ^ n))";
 by (dres_inst_tac [("z","abs z")] powser_insidea 1);
 by (auto_tac (claset() addIs [summable_rabs_cancel],
-    simpset() addsimps [realpow_abs,abs_mult RS sym]));
+    simpset() addsimps [realpow_abs RS sym,abs_mult RS sym]));
 qed "powser_inside";
 
 (* ------------------------------------------------------------------------ *)
@@ -597,7 +597,7 @@
 by (auto_tac (claset() addSIs [real_mult_le_mono],simpset() addsimps 
     [abs_ge_zero] delsimps [sumr_Suc])); 
 by (auto_tac (claset() addSIs [realpow_le2],simpset() addsimps 
-    [realpow_abs RS sym,abs_ge_zero] delsimps [sumr_Suc] ));
+    [realpow_abs,abs_ge_zero] delsimps [sumr_Suc] ));
 by (res_inst_tac [("j","real (Suc d) * (K ^ d)")] real_le_trans 1);
 by (subgoal_tac "0 <= K" 2);
 by (arith_tac 3);
@@ -609,7 +609,7 @@
     addSIs [real_mult_le_mono],simpset() addsimps [abs_mult,
     realpow_add,abs_ge_zero]));
 by (auto_tac (claset() addSIs [realpow_le2,realpow_ge_zero],simpset() addsimps 
-    [realpow_abs RS sym,abs_ge_zero]));
+    [realpow_abs,abs_ge_zero]));
 by (ALLGOALS(arith_tac));
 qed "lemma_termdiff3";
 
diff -r 8743e8305611 -r c69bee072501 src/HOL/Real/RealPow.ML
--- a/src/HOL/Real/RealPow.ML	Thu Nov 29 17:39:23 2001 +0100
+++ b/src/HOL/Real/RealPow.ML	Thu Nov 29 19:03:03 2001 +0100
@@ -29,7 +29,7 @@
 by (auto_tac (claset(), simpset() addsimps [real_inverse_distrib]));
 qed "realpow_inverse";
 
-Goal "abs (r::real) ^ n = abs (r ^ n)";
+Goal "abs(r ^ n) = abs(r::real) ^ n";
 by (induct_tac "n" 1);
 by (auto_tac (claset(), simpset() addsimps [abs_mult]));
 qed "realpow_abs";
@@ -101,7 +101,7 @@
 Addsimps [abs_realpow_two];
 
 Goal "abs(x::real)^Suc (Suc 0) = x^Suc (Suc 0)";
-by (simp_tac (simpset() addsimps [realpow_abs,abs_eqI1]
+by (simp_tac (simpset() addsimps [realpow_abs RS sym,abs_eqI1]
                         delsimps [realpow_Suc]) 1);
 qed "realpow_two_abs";
 Addsimps [realpow_two_abs];