# HG changeset patch
# User paulson
# Date 977310952 -3600
# Node ID 351ba950d4d9b42bc37edcf65714ecfddeca40c9
# Parent  a9f6994fb90665321f431da9cc319c4732fd81c6
further tidying

diff -r a9f6994fb906 -r 351ba950d4d9 src/HOL/Real/Hyperreal/HSeries.ML
--- a/src/HOL/Real/Hyperreal/HSeries.ML	Wed Dec 20 12:14:50 2000 +0100
+++ b/src/HOL/Real/Hyperreal/HSeries.ML	Wed Dec 20 12:15:52 2000 +0100
@@ -187,13 +187,6 @@
          real_of_nat_def,hypreal_minus,hypreal_add]));
 qed "sumhr_hypreal_omega_minus_one";
 
-(***??SERIES.ML??replace old versions???*)
-Goal "sumr 0 (#2*n) (%i. (#-1) ^ Suc i) = #0";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed "sumr_minus_one_realpow_zero";
-Addsimps [sumr_minus_one_realpow_zero];
-
 Goalw [hypnat_zero_def, hypnat_omega_def, hypreal_zero_def]
      "sumhr(0, whn + whn, %i. (-#1) ^ (i+1)) = 0";
 by (simp_tac (simpset() addsimps [sumhr,hypnat_add] 
diff -r a9f6994fb906 -r 351ba950d4d9 src/HOL/Real/Hyperreal/HyperDef.ML
--- a/src/HOL/Real/Hyperreal/HyperDef.ML	Wed Dec 20 12:14:50 2000 +0100
+++ b/src/HOL/Real/Hyperreal/HyperDef.ML	Wed Dec 20 12:15:52 2000 +0100
@@ -930,13 +930,9 @@
 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
 qed "hypreal_eq_minus_iff3";
 
-Goal "(x = z + y) = (x + -z = (y::hypreal))";
-by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
-qed "hypreal_eq_minus_iff4";
-
 Goal "(x ~= a) = (x + -a ~= (0::hypreal))";
-by (auto_tac (claset() addDs [sym RS 
-    (hypreal_eq_minus_iff RS iffD2)],simpset())); 
+by (auto_tac (claset() addDs [sym RS (hypreal_eq_minus_iff RS iffD2)],
+              simpset())); 
 qed "hypreal_not_eq_minus_iff";
 
 (*** linearity ***)
@@ -1074,6 +1070,7 @@
 by (simp_tac (simpset() addsimps 
     [hypreal_minus_zero_less_iff2]) 1);
 qed "hypreal_minus_zero_le_iff";
+Addsimps [hypreal_minus_zero_le_iff];
 
 (*----------------------------------------------------------
   hypreal_of_real preserves field and order properties
@@ -1305,11 +1302,6 @@
 qed "hypreal_mult_self_eq_zero_iff";
 Addsimps [hypreal_mult_self_eq_zero_iff];
 
-Goal "(0 = x * x) = (x = (0::hypreal))";
-by (auto_tac (claset() addDs [sym],simpset()));
-qed "hypreal_mult_self_eq_zero_iff2";
-Addsimps [hypreal_mult_self_eq_zero_iff2];
-
 Goalw [hypreal_diff_def] "(x<y) = (x-y < (0::hypreal))";
 by (rtac hypreal_less_minus_iff2 1);
 qed "hypreal_less_eq_diff";
diff -r a9f6994fb906 -r 351ba950d4d9 src/HOL/Real/Hyperreal/HyperOrd.ML
--- a/src/HOL/Real/Hyperreal/HyperOrd.ML	Wed Dec 20 12:14:50 2000 +0100
+++ b/src/HOL/Real/Hyperreal/HyperOrd.ML	Wed Dec 20 12:15:52 2000 +0100
@@ -176,8 +176,8 @@
 Goalw [hypreal_one_def,hypreal_zero_def,hypreal_less_def] "0 < 1hr";
 by (res_inst_tac [("x","%n. #0")] exI 1);
 by (res_inst_tac [("x","%n. #1")] exI 1);
-by (auto_tac (claset(),simpset() addsimps [real_zero_less_one,
-    FreeUltrafilterNat_Nat_set]));
+by (auto_tac (claset(),
+        simpset() addsimps [real_zero_less_one, FreeUltrafilterNat_Nat_set]));
 qed "hypreal_zero_less_one";
 
 Goal "1hr < 1hr + 1hr";
@@ -428,52 +428,28 @@
 qed "hypreal_dense";
 
 
-Goal "(x*x + y*y = 0) = (x = 0 & y = (0::hypreal))";
+(*?? more needed and earlier??*)
+Goal "(x+y = (0::hypreal)) = (x = -y)";
+by (stac hypreal_eq_minus_iff 1);
 by Auto_tac;
-by (dtac (sym RS (hypreal_eq_minus_iff3 RS iffD1))  1);
-by (dtac (sym RS (hypreal_eq_minus_iff4 RS iffD1))  2);
-by (ALLGOALS(rtac ccontr));
-by (ALLGOALS(dtac hypreal_mult_self_not_zero));
-by (cut_inst_tac [("x1","x")] (hypreal_le_square 
-        RS hypreal_le_imp_less_or_eq) 1);
-by (cut_inst_tac [("x1","y")] (hypreal_le_square 
-        RS hypreal_le_imp_less_or_eq) 2);
-by (auto_tac (claset() addDs [sym],simpset()));
-by (dres_inst_tac [("x1","y")] (hypreal_less_minus_square 
-    RS hypreal_le_less_trans) 1);
-by (dres_inst_tac [("x1","x")] (hypreal_less_minus_square 
-    RS hypreal_le_less_trans) 2);
-by (auto_tac (claset(),simpset() addsimps 
-       [hypreal_less_not_refl]));
+qed "hypreal_add_eq_0_iff";
+AddIffs [hypreal_add_eq_0_iff];
+
+Goal "[| 0 <= x; 0 <= y |] ==> (x+y = 0) = (x = 0 & y = (0::hypreal))";
+by (auto_tac (claset() addIs [order_antisym], simpset()));
+qed "hypreal_add_nonneg_eq_0_iff";
+
+Goal "(x*x + y*y = 0) = (x = 0 & y = (0::hypreal))";
+by (simp_tac
+    (HOL_ss addsimps [hypreal_le_square, hypreal_add_nonneg_eq_0_iff]) 1);
+by Auto_tac;
 qed "hypreal_squares_add_zero_iff";
 Addsimps [hypreal_squares_add_zero_iff];
 
-Goal "x * x ~= 0 ==> (0::hypreal) < x* x + y*y + z*z";
-by (cut_inst_tac [("x1","x")] (hypreal_le_square 
-        RS hypreal_le_imp_less_or_eq) 1);
-by (auto_tac (claset() addSIs [hypreal_add_order_le],
-              simpset()));
-qed "hypreal_sum_squares3_gt_zero";
-
-Goal "x * x ~= 0 ==> (0::hypreal) < y*y + x*x + z*z";
-by (dtac hypreal_sum_squares3_gt_zero 1);
-by (auto_tac (claset(), simpset() addsimps hypreal_add_ac));
-qed "hypreal_sum_squares3_gt_zero2";
-
-Goal "x * x ~= 0 ==> (0::hypreal) < y*y + z*z + x*x";
-by (dtac hypreal_sum_squares3_gt_zero 1);
-by (auto_tac (claset(), simpset() addsimps hypreal_add_ac));
-qed "hypreal_sum_squares3_gt_zero3";
-
-
 Goal "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))";
+by (simp_tac (HOL_ss addsimps [hypreal_le_square, hypreal_le_add_order, 
+                               hypreal_add_nonneg_eq_0_iff]) 1);
 by Auto_tac;
-by (ALLGOALS(rtac ccontr));
-by (ALLGOALS(dtac hypreal_mult_self_not_zero));
-by (auto_tac (claset() addDs [hypreal_not_refl2 RS not_sym,
-   hypreal_sum_squares3_gt_zero3,hypreal_sum_squares3_gt_zero,
-   hypreal_sum_squares3_gt_zero2],simpset() delsimps
-   [hypreal_mult_self_eq_zero_iff]));
 qed "hypreal_three_squares_add_zero_iff";
 Addsimps [hypreal_three_squares_add_zero_iff];
 
@@ -758,11 +734,12 @@
  ----------------------------------------------------------------------------*)
 
 Goal "((0::hypreal) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)";
- by (auto_tac (claset(), simpset() addsimps [order_le_less, 
-    linorder_not_less, hypreal_mult_order, hypreal_mult_less_zero1]));
+ by (auto_tac (claset(), 
+               simpset() addsimps [order_le_less, linorder_not_less, 
+                              hypreal_mult_order, hypreal_mult_less_zero1]));
 by (ALLGOALS (rtac ccontr)); 
-by (auto_tac (claset(), simpset() addsimps 
-    [order_le_less, linorder_not_less]));
+by (auto_tac (claset(), 
+              simpset() addsimps [order_le_less, linorder_not_less]));
 by (ALLGOALS (etac rev_mp)); 
 by (ALLGOALS (dtac hypreal_mult_less_zero THEN' assume_tac));
 by (auto_tac (claset() addDs [order_less_not_sym], 
@@ -770,9 +747,9 @@
 qed "hypreal_zero_less_mult_iff";
 
 Goal "((0::hypreal) <= x*y) = (0 <= x & 0 <= y | x <= 0 & y <= 0)";
-by (auto_tac (claset() addDs [sym RS hypreal_mult_zero_disj],
-    simpset() addsimps [order_le_less,
-    linorder_not_less,hypreal_zero_less_mult_iff]));
+by (auto_tac (claset() addDs [hypreal_mult_zero_disj],
+              simpset() addsimps [order_le_less, linorder_not_less,
+                                  hypreal_zero_less_mult_iff]));
 qed "hypreal_zero_le_mult_iff";
 
 Goal "(x*y < (0::hypreal)) = (0 < x & y < 0 | x < 0 & 0 < y)";
diff -r a9f6994fb906 -r 351ba950d4d9 src/HOL/Real/Hyperreal/HyperPow.ML
--- a/src/HOL/Real/Hyperreal/HyperPow.ML	Wed Dec 20 12:14:50 2000 +0100
+++ b/src/HOL/Real/Hyperreal/HyperPow.ML	Wed Dec 20 12:15:52 2000 +0100
@@ -114,10 +114,9 @@
 qed "hrealpow_two_le_add_order2";
 Addsimps [hrealpow_two_le_add_order2];
 
-(* See HYPER.ML *)
-Goal "(x ^ 2 + y ^ 2 + z ^ 2 = (0::hypreal)) = \ 
-\               (x = 0 & y = 0 & z = 0)";
-by (simp_tac (simpset() addsimps [hrealpow_two]) 1);
+Goal "(x ^ 2 + y ^ 2 + z ^ 2 = (0::hypreal)) = (x = 0 & y = 0 & z = 0)";
+by (simp_tac (HOL_ss addsimps [hypreal_three_squares_add_zero_iff, 
+                               hrealpow_two]) 1);
 qed "hrealpow_three_squares_add_zero_iff";
 Addsimps [hrealpow_three_squares_add_zero_iff];
 
@@ -127,8 +126,8 @@
 Addsimps [hrabs_hrealpow_two];
 
 Goal "abs(x) ^ 2 = (x::hypreal) ^ 2";
-by (simp_tac (simpset() addsimps [hrealpow_hrabs,
-    hrabs_eqI1] delsimps [hpowr_Suc]) 1);
+by (simp_tac (simpset() addsimps [hrealpow_hrabs, hrabs_eqI1] 
+                        delsimps [hpowr_Suc]) 1);
 qed "hrealpow_two_hrabs";
 Addsimps [hrealpow_two_hrabs];
 
diff -r a9f6994fb906 -r 351ba950d4d9 src/HOL/Real/Hyperreal/Lim.ML
--- a/src/HOL/Real/Hyperreal/Lim.ML	Wed Dec 20 12:14:50 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Lim.ML	Wed Dec 20 12:15:52 2000 +0100
@@ -6,24 +6,11 @@
 *)
 
 
-(*DELETE?????*)
 fun ARITH_PROVE str = prove_goal thy str 
                       (fn prems => [cut_facts_tac prems 1,arith_tac 1]);
 
 
 
-(***?REALARITH.ML?? also below??*)
-Goal "(x + - a = (#0::real)) = (x=a)";
-by (arith_tac 1);
-qed "real_add_minus_iff";
-Addsimps [real_add_minus_iff];
-
-Goal "(-b = -a) = (b = (a::real))";
-by (arith_tac 1);
-qed "real_minus_eq_cancel";
-Addsimps [real_minus_eq_cancel];
-
-
 (*---------------------------------------------------------------
    Theory of limits, continuity and differentiation of 
    real=>real functions 
@@ -545,23 +532,21 @@
  --------------------------------------------------------------------------*)
 (* Prove equivalence between NS limits - *)
 (* seems easier than using standard def  *)
-Goalw [NSLIM_def] 
-      "(f -- a --NS> L) = ((%h. f(a + h)) -- #0 --NS> L)";
+Goalw [NSLIM_def] "(f -- a --NS> L) = ((%h. f(a + h)) -- #0 --NS> L)";
 by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_zero]));
 by (dres_inst_tac [("x","hypreal_of_real a + x")] spec 1);
 by (dres_inst_tac [("x","-hypreal_of_real a + x")] spec 2);
 by (Step_tac 1);
-by (dtac (sym RS (hypreal_eq_minus_iff4 RS iffD1)) 1);
+by (Asm_full_simp_tac 1);
 by (rtac ((mem_infmal_iff RS iffD2) RS 
-    (Infinitesimal_add_inf_close_self RS inf_close_sym)) 2);
-by (rtac (inf_close_minus_iff2 RS iffD1) 5);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 4);
-by (dtac (sym RS (hypreal_eq_minus_iff RS iffD2)) 4);
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 3);
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 6);
-by (auto_tac (claset(),simpset() addsimps [starfun,
-    hypreal_of_real_def,hypreal_minus,hypreal_add,
-    real_add_assoc,inf_close_refl,hypreal_zero_def]));
+    (Infinitesimal_add_inf_close_self RS inf_close_sym)) 1);
+by (rtac (inf_close_minus_iff2 RS iffD1) 4);
+by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 3);
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 2);
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 4);
+by (auto_tac (claset(),
+       simpset() addsimps [starfun, hypreal_of_real_def, hypreal_minus,
+              hypreal_add, real_add_assoc, inf_close_refl, hypreal_zero_def]));
 qed "NSLIM_h_iff";
 
 Goal "(f -- a --NS> f a) = ((%h. f(a + h)) -- #0 --NS> f a)";
@@ -569,12 +554,10 @@
 qed "NSLIM_isCont_iff";
 
 Goal "(f -- a --> f a) = ((%h. f(a + h)) -- #0 --> f(a))";
-by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff,
-    NSLIM_isCont_iff]) 1);
+by (simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_isCont_iff]) 1);
 qed "LIM_isCont_iff";
 
-Goalw [isCont_def] 
-      "(isCont f x) = ((%h. f(x + h)) -- #0 --> f(x))";
+Goalw [isCont_def] "(isCont f x) = ((%h. f(x + h)) -- #0 --> f(x))";
 by (simp_tac (simpset() addsimps [LIM_isCont_iff]) 1);
 qed "isCont_iff";
 
@@ -1414,6 +1397,22 @@
  ---------------------------------------------------------------*)
 
 
+
+(*??REPLACE THE ONE IN HYPERDEF*??*)
+Goal "inverse(x*y) = inverse(x)*inverse(y::hypreal)";
+by (case_tac "x=0 | y=0" 1);
+by (force_tac (claset(), simpset() addsimps [HYPREAL_INVERSE_ZERO]) 1); 
+by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1);
+by (auto_tac (claset(),
+        simpset() addsimps [hypreal_mult_assoc RS sym, hypreal_mult_not_0]));
+by (res_inst_tac [("c1","y")] (hypreal_mult_right_cancel RS iffD1) 1);
+by (auto_tac (claset(),
+        simpset() addsimps [hypreal_mult_not_0] @ hypreal_mult_ac));
+by (auto_tac (claset(),
+        simpset() addsimps [hypreal_mult_assoc RS sym, hypreal_mult_not_0]));
+qed "inverse_mult_eq";
+
+(**?? FIXME messy proof, needs simprocs! ??*)
 (*Can't get rid of x ~= #0 because it isn't continuous at zero*)
 Goalw [nsderiv_def]
      "x ~= #0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))";
@@ -1427,13 +1426,26 @@
                delsimps [hypreal_minus_mult_eq1 RS sym,
                          hypreal_minus_mult_eq2 RS sym]));
 by (dtac (hypreal_of_real_not_zero_iff RS iffD2) 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse_add,
-         inverse_mult_eq RS sym, hypreal_minus_inverse RS sym] 
-         @ hypreal_add_ac @ hypreal_mult_ac delsimps [hypreal_minus_mult_eq1 RS
-         sym,hypreal_minus_mult_eq2 RS sym] ) 1);
+by (asm_full_simp_tac
+     (simpset() addsimps [hypreal_inverse_add,
+          inverse_mult_eq RS sym, hypreal_minus_inverse RS sym] 
+          @ hypreal_add_ac @ hypreal_mult_ac 
+       delsimps [hypreal_minus_mult_eq1 RS sym,
+                 hypreal_minus_mult_eq2 RS sym] ) 1);
+by (stac hypreal_inverse_add 1); 
+by (asm_full_simp_tac (simpset() addsimps []) 1);
+by (stac hypreal_add_commute 1);  
+by (asm_simp_tac (simpset() addsimps []) 1); 
+by (asm_full_simp_tac
+     (simpset() addsimps [hypreal_inverse_add,
+          inverse_mult_eq RS sym, hypreal_minus_inverse RS sym] 
+          @ hypreal_add_ac @ hypreal_mult_ac 
+       delsimps [hypreal_minus_mult_eq1 RS sym,
+                 hypreal_minus_mult_eq2 RS sym] ) 1);
 by (asm_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym,
-         hypreal_add_mult_distrib2] delsimps [hypreal_minus_mult_eq1 RS
-         sym,hypreal_minus_mult_eq2 RS sym]) 1);
+                                      hypreal_add_mult_distrib2] 
+         delsimps [hypreal_minus_mult_eq1 RS sym, 
+                   hypreal_minus_mult_eq2 RS sym]) 1);
 by (dres_inst_tac [("x3","x") ] ((HFinite_hypreal_of_real RSN
          (2,Infinitesimal_HFinite_mult2)) RS  
           (Infinitesimal_minus_iff RS iffD1)) 1); 
@@ -1446,6 +1458,8 @@
          [hypreal_minus_inverse RS sym,hypreal_of_real_mult RS sym]));
 qed "NSDERIV_inverse";
 
+
+
 Goal "x ~= #0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ 2))";
 by (asm_simp_tac (simpset() addsimps [NSDERIV_inverse,
          NSDERIV_DERIV_iff RS sym] delsimps [realpow_Suc]) 1);
@@ -1769,14 +1783,6 @@
 (* Intermediate Value Theorem (prove contrapositive by bisection)             *)
 (*----------------------------------------------------------------------------*)
 
-
-    (*ALREADY IN REALABS.ML????????????????*)
-    Goalw [abs_real_def] "(abs x = #0) = (x=(#0::real))";
-    by (Full_simp_tac 1);
-    qed "abs_zero_iff";
-    AddIffs [abs_zero_iff];
-
-
 Goal "[| f(a) <= y & y <= f(b); \
 \        a <= b; \
 \        (ALL x. a <= x & x <= b --> isCont f x) |] \
@@ -1899,8 +1905,6 @@
 by (res_inst_tac [("j","abs(f x) + abs(f(xa) - f(x))")] real_le_trans 4);
 by (auto_tac (claset() addIs [abs_triangle_ineq RSN (2, real_le_trans)],
               simpset() addsimps [real_diff_def,abs_ge_self]));
-(*arith_tac problem: this step should not be needed*)
-by (asm_full_simp_tac (simpset() addsimps [rename_numerals (real_eq_minus_iff2 RS sym)]) 1);
 by (auto_tac (claset(),
               simpset() addsimps [abs_real_def] addsplits [split_if_asm]));
 qed "isCont_bounded";
diff -r a9f6994fb906 -r 351ba950d4d9 src/HOL/Real/Hyperreal/NSA.ML
--- a/src/HOL/Real/Hyperreal/NSA.ML	Wed Dec 20 12:14:50 2000 +0100
+++ b/src/HOL/Real/Hyperreal/NSA.ML	Wed Dec 20 12:15:52 2000 +0100
@@ -93,19 +93,19 @@
 qed "SReal_omega_not_mem";
 
 Goalw [SReal_def] "{x. hypreal_of_real x : SReal} = (UNIV::real set)";
-by (Auto_tac);
+by Auto_tac;
 qed "SReal_UNIV_real";
 
 Goalw [SReal_def] "(x: SReal) = (EX y. x = hypreal_of_real  y)";
-by (Auto_tac);
+by Auto_tac;
 qed "SReal_iff";
 
 Goalw [SReal_def] "hypreal_of_real ``(UNIV::real set) = SReal";
-by (Auto_tac);
+by Auto_tac;
 qed "hypreal_of_real_image";
 
 Goalw [SReal_def] "inv hypreal_of_real ``SReal = (UNIV::real set)";
-by (Auto_tac);
+by Auto_tac;
 by (rtac (inj_hypreal_of_real RS inv_f_f RS subst) 1);
 by (Blast_tac 1);
 qed "inv_hypreal_of_real_image";
@@ -119,7 +119,7 @@
 by (auto_tac (claset(),simpset() addsimps [SReal_iff]));
 by (dtac real_dense 1 THEN Step_tac 1);
 by (res_inst_tac [("x","hypreal_of_real r")] bexI 1);
-by (Auto_tac);
+by Auto_tac;
 qed "SReal_dense";
 
 (*------------------------------------------------------------------
@@ -195,7 +195,7 @@
 Goalw [isLub_def,leastP_def,isUb_def] 
       "EX Yo. isLub SReal P (hypreal_of_real Yo) \
 \      ==> EX Y. isLub SReal P Y";
-by (Auto_tac);
+by Auto_tac;
 qed "lemma_isLub_hypreal_of_real2";
 
 Goal "[| P <= SReal; EX x. x: P; \
@@ -243,7 +243,7 @@
 Addsimps [HFinite_hypreal_of_real];
 
 Goalw [HFinite_def] "x : HFinite ==> EX t: SReal. abs x < t";
-by (Auto_tac);
+by Auto_tac;
 qed "HFiniteD";
 
 Goalw [HFinite_def] "x : HFinite ==> abs x : HFinite";
@@ -279,7 +279,7 @@
  ------------------------------------------------------------------*)
 Goalw [Infinitesimal_def]
       "x : Infinitesimal ==> ALL r: SReal. 0 < r --> abs x < r";
-by (Auto_tac);
+by Auto_tac;
 qed "InfinitesimalD";
 
 Goalw [Infinitesimal_def] "0 : Infinitesimal";
@@ -289,7 +289,7 @@
 
 Goalw [Infinitesimal_def] 
       "[| x : Infinitesimal; y : Infinitesimal |] ==> (x + y) : Infinitesimal";
-by (Auto_tac);
+by Auto_tac;
 by (rtac (hypreal_sum_of_halves RS subst) 1);
 by (dtac hypreal_half_gt_zero 1);
 by (dtac SReal_half 1);
@@ -314,7 +314,7 @@
 Goalw [Infinitesimal_def] 
       "[| x : Infinitesimal; y : Infinitesimal |] \
 \      ==> (x * y) : Infinitesimal";
-by (Auto_tac);
+by Auto_tac;
 by (rtac (hypreal_mult_1_right RS subst) 1);
 by (rtac hrabs_mult_less 1);
 by (cut_facts_tac [SReal_one,hypreal_zero_less_one] 2);
@@ -346,7 +346,7 @@
 (*** rather long proof ***)
 Goalw [HInfinite_def,Infinitesimal_def] 
      "x: HInfinite ==> inverse x: Infinitesimal";
-by (Auto_tac);
+by Auto_tac;
 by (eres_inst_tac [("x","inverse r")] ballE 1);
 by (rtac (hrabs_inverse RS ssubst) 1);
 by (forw_inst_tac [("x1","r"),("R3.0","abs x")] 
@@ -363,7 +363,7 @@
 
 Goalw [HInfinite_def] 
    "[|x: HInfinite;y: HInfinite|] ==> (x*y): HInfinite";
-by (Auto_tac);
+by Auto_tac;
 by (cut_facts_tac [SReal_one] 1);
 by (eres_inst_tac [("x","1hr")] ballE 1);
 by (eres_inst_tac [("x","r")] ballE 1);
@@ -388,39 +388,34 @@
     hypreal_less_imp_le]) 1);
 qed "HInfinite_add_gt_zero";
 
-Goalw [HInfinite_def] 
-     "(-x: HInfinite) = (x: HInfinite)";
+Goalw [HInfinite_def] "(-x: HInfinite) = (x: HInfinite)";
 by (auto_tac (claset(),simpset() addsimps 
     [hrabs_minus_cancel]));
 qed "HInfinite_minus_iff";
 
-Goal "[|x: HInfinite; y <= 0; x <= 0|] \
-\      ==> (x + y): HInfinite";
+Goal "[|x: HInfinite; y <= 0; x <= 0|] ==> (x + y): HInfinite";
 by (dtac (HInfinite_minus_iff RS iffD2) 1);
 by (rtac (HInfinite_minus_iff RS iffD1) 1);
 by (auto_tac (claset() addIs [HInfinite_add_ge_zero],
-    simpset() addsimps [hypreal_minus_zero_le_iff RS sym,
-    hypreal_minus_add_distrib]));
+              simpset() addsimps [hypreal_minus_zero_le_iff]));
 qed "HInfinite_add_le_zero";
 
-Goal "[|x: HInfinite; y < 0; x < 0|] \
-\      ==> (x + y): HInfinite";
+Goal "[|x: HInfinite; y < 0; x < 0|] ==> (x + y): HInfinite";
 by (blast_tac (claset() addIs [HInfinite_add_le_zero,
-    hypreal_less_imp_le]) 1);
+                               hypreal_less_imp_le]) 1);
 qed "HInfinite_add_lt_zero";
 
 Goal "[|a: HFinite; b: HFinite; c: HFinite|] \ 
 \     ==> a*a + b*b + c*c : HFinite";
-by (auto_tac (claset() addIs [HFinite_mult,HFinite_add],
-    simpset()));
+by (auto_tac (claset() addIs [HFinite_mult,HFinite_add], simpset()));
 qed "HFinite_sum_squares";
 
 Goal "x ~: Infinitesimal ==> x ~= 0";
-by (Auto_tac);
+by Auto_tac;
 qed "not_Infinitesimal_not_zero";
 
 Goal "x: HFinite - Infinitesimal ==> x ~= 0";
-by (Auto_tac);
+by Auto_tac;
 qed "not_Infinitesimal_not_zero2";
 
 Goal "x : Infinitesimal ==> abs x : Infinitesimal";
@@ -652,8 +647,8 @@
 qed "bex_Infinitesimal_iff";
 
 Goal "(EX y: Infinitesimal. x = z + y) = (x @= z)";
-by (asm_full_simp_tac (simpset() addsimps [hypreal_eq_minus_iff4,
-    bex_Infinitesimal_iff RS sym]) 1);
+by (asm_full_simp_tac (simpset() addsimps [bex_Infinitesimal_iff RS sym]) 1);
+by (Force_tac 1);
 qed "bex_Infinitesimal_iff2";
 
 Goal "[| y: Infinitesimal; x + y = z |] ==> x @= z";
@@ -742,7 +737,7 @@
 
 Goal "x @= hypreal_of_real D ==> x: HFinite";
 by (rtac (inf_close_sym RSN (2,inf_close_HFinite)) 1);
-by (Auto_tac);
+by Auto_tac;
 qed "inf_close_hypreal_of_real_HFinite";
 
 Goal "[|a @= hypreal_of_real b; c @= hypreal_of_real d |] \
@@ -788,7 +783,7 @@
 
 Goal "[| z <= f; f @= g; g <= z |] ==> f @= z";
 by (dtac (bex_Infinitesimal_iff2 RS iffD2) 1);
-by (Auto_tac);
+by Auto_tac;
 by (dres_inst_tac [("x","-g")] hypreal_add_left_le_mono1 1);
 by (dres_inst_tac [("x","-g")] hypreal_add_le_mono1 1);
 by (res_inst_tac [("y","-y")] Infinitesimal_add_cancel 1);
@@ -862,30 +857,30 @@
 
 Goal "hypreal_of_real x ~= 0 ==> hypreal_of_real x : HFinite - Infinitesimal";
 by (rtac SReal_HFinite_diff_Infinitesimal 1);
-by (Auto_tac);
+by Auto_tac;
 qed "hypreal_of_real_HFinite_diff_Infinitesimal";
 
 Goal "1hr+1hr ~: Infinitesimal";
-by (fast_tac (claset() addIs [SReal_two RS SReal_Infinitesimal_zero,
-    hypreal_two_not_zero RS notE]) 1);
+by (fast_tac (claset() addDs [SReal_two RS SReal_Infinitesimal_zero]
+                       addSEs [hypreal_two_not_zero RS notE]) 1);
 qed "two_not_Infinitesimal";
 
 Goal "1hr ~: Infinitesimal";
 by (auto_tac (claset() addSDs [SReal_one RS SReal_Infinitesimal_zero],
-    simpset() addsimps [hypreal_zero_not_eq_one RS not_sym]));
+                simpset() addsimps [hypreal_zero_not_eq_one RS not_sym]));
 qed "hypreal_one_not_Infinitesimal";
 Addsimps [hypreal_one_not_Infinitesimal];
 
 Goal "[| y: SReal; x @= y; y~= 0 |] ==> x ~= 0";
 by (cut_inst_tac [("x","y")] hypreal_trichotomy 1);
 by (blast_tac (claset() addDs 
-    [inf_close_sym RS (mem_infmal_iff RS iffD2),
-     SReal_not_Infinitesimal,SReal_minus_not_Infinitesimal]) 1);
+		[inf_close_sym RS (mem_infmal_iff RS iffD2),
+		 SReal_not_Infinitesimal,SReal_minus_not_Infinitesimal]) 1);
 qed "inf_close_SReal_not_zero";
 
 Goal "[| x @= hypreal_of_real y; hypreal_of_real y ~= 0 |] ==> x ~= 0";
 by (rtac inf_close_SReal_not_zero 1);
-by (Auto_tac);
+by Auto_tac;
 qed "inf_close_hypreal_of_real_not_zero";
 
 Goal "[| x @= y; y : HFinite - Infinitesimal |] \
@@ -960,7 +955,7 @@
 qed "lemma_st_part_nonempty";
 
 Goal "{s. s: SReal & s < x} <= SReal";
-by (Auto_tac);
+by Auto_tac;
 qed "lemma_st_part_subset";
 
 Goal "x: HFinite ==> EX t. isLub SReal {s. s: SReal & s < x} t";
@@ -1007,8 +1002,6 @@
 Goal "t <= t + -r ==> r <= (0::hypreal)";
 by (dres_inst_tac [("x","-t")] hypreal_add_left_le_mono1 1);
 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc RS sym]));
-by (dres_inst_tac [("x","r")] hypreal_add_left_le_mono1 1);
-by (Auto_tac);
 qed "lemma_minus_le_zero";
 
 Goal "[| x: HFinite; \
@@ -1075,7 +1068,7 @@
 \        isLub SReal {s. s: SReal & s < x} t; \
 \        r: SReal; 0 < r |] \
 \     ==> x + -t ~= r";
-by (Auto_tac);
+by Auto_tac;
 by (forward_tac [isLubD1a RS SReal_minus] 1);
 by (dtac SReal_add_cancel 1 THEN assume_tac 1);
 by (dres_inst_tac [("x","x")] lemma_SReal_lub 1);
@@ -1103,7 +1096,7 @@
 \     ==> abs (x + -t) < r";
 by (forward_tac [lemma_st_part1a] 1);
 by (forward_tac [lemma_st_part2a] 4);
-by (Auto_tac);
+by Auto_tac;
 by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
 by (auto_tac (claset() addDs [lemma_st_part_not_eq1,
     lemma_st_part_not_eq2],simpset() addsimps [hrabs_interval_iff2]));
@@ -1153,7 +1146,7 @@
 
 Goal "x: HFinite ==> x ~: HInfinite";
 by (EVERY1[Step_tac, dtac IntI, assume_tac]);
-by (Auto_tac);
+by Auto_tac;
 qed "HFinite_not_HInfinite";
 
 val [prem] = goalw thy [HInfinite_def] "x~: HFinite ==> x: HInfinite";
@@ -1219,7 +1212,7 @@
 by (forw_inst_tac [("x","x")] not_Infinitesimal_not_zero2 1);
 by (REPEAT(dtac HFinite_inverse2 1));
 by (dtac inf_close_mult2 1 THEN assume_tac 1);
-by (Auto_tac);
+by Auto_tac;
 by (dres_inst_tac [("c","inverse x")] inf_close_mult1 1 
     THEN assume_tac 1);
 by (auto_tac (claset() addIs [inf_close_sym],
@@ -1296,7 +1289,7 @@
 
 Goal "monad (abs x) <= monad(x) Un monad(-x)";
 by (res_inst_tac [("x1","x")] (hrabs_disj RS disjE) 1);
-by (Auto_tac);
+by Auto_tac;
 qed "monad_hrabs_Un_subset";
 
 Goal "!! e. e : Infinitesimal ==> monad (x+e) = monad x";
@@ -1305,7 +1298,7 @@
 qed "Infinitesimal_monad_eq";
 
 Goalw [monad_def] "(u:monad x) = (-u:monad (-x))";
-by (Auto_tac);
+by Auto_tac;
 qed "mem_monad_iff";
 
 Goalw [monad_def] "(x:Infinitesimal) = (x:monad 0)";
@@ -1408,7 +1401,7 @@
 by (forward_tac [lemma_inf_close_less_zero] 1);
 by (REPEAT(assume_tac 1));
 by (REPEAT(dtac hrabs_minus_eqI2 1));
-by (Auto_tac);
+by Auto_tac;
 qed "inf_close_hrabs1";
 
 Goal "[| x @= y; 0 < x; x ~: Infinitesimal |] \
@@ -1416,7 +1409,7 @@
 by (forward_tac [lemma_inf_close_gt_zero] 1);
 by (REPEAT(assume_tac 1));
 by (REPEAT(dtac hrabs_eqI2 1));
-by (Auto_tac);
+by Auto_tac;
 qed "inf_close_hrabs2";
 
 Goal "x @= y ==> abs x @= abs y";
@@ -1865,16 +1858,16 @@
 Goal "[| X: Rep_hypreal x; Y: Rep_hypreal x |] \
 \              ==> {n. X n = Y n} : FreeUltrafilterNat";
 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (Auto_tac);
+by Auto_tac;
 by (Ultra_tac 1);
 qed "FreeUltrafilterNat_Rep_hypreal";
 
 Goal "{n. Yb n < Y n} Int {n. -y = Yb n} <= {n. -y < Y n}";
-by (Auto_tac);
+by Auto_tac;
 qed "lemma_free1";
 
 Goal "{n. Xa n < Yc n} Int {n. y = Yc n} <= {n. Xa n < y}";
-by (Auto_tac);
+by Auto_tac;
 qed "lemma_free2";
 
 Goalw [HFinite_def] 
@@ -1950,7 +1943,7 @@
 by (auto_tac (claset(),simpset() delsimps [Rep_hypreal_nonempty] 
     addsimps [HFinite_FreeUltrafilterNat_iff,Bex_def]));
 by (REPEAT(dtac spec 1));
-by (Auto_tac);
+by Auto_tac;
 by (dres_inst_tac [("x","u")] spec 1 THEN 
     REPEAT(dtac FreeUltrafilterNat_Compl_mem 1));
 by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
@@ -1965,7 +1958,7 @@
 (* yet more lemmas! *)
 Goal "{n. abs (Xa n) < u} Int {n. X n = Xa n} \
 \         <= {n. abs (X n) < (u::real)}";
-by (Auto_tac);
+by Auto_tac;
 qed "lemma_Int_HI";
 
 Goal "{n. u < abs (X n)} Int {n. abs (X n) < (u::real)} = {}";
@@ -1977,7 +1970,7 @@
 \              ==>  x : HInfinite";
 by (rtac (HInfinite_HFinite_iff RS iffD2) 1);
 by (Step_tac 1 THEN dtac HFinite_FreeUltrafilterNat 1);
-by (Auto_tac);
+by Auto_tac;
 by (dres_inst_tac [("x","u")] spec 1);
 by (dtac FreeUltrafilterNat_Rep_hypreal 1 THEN assume_tac 1);
 by (dres_inst_tac [("Y","{n. X n = Xa n}")] FreeUltrafilterNat_Int 1);
@@ -1998,11 +1991,11 @@
  --------------------------------------------------------------------*)
 
 Goal "{n. - u < Yd n} Int {n. xa n = Yd n} <= {n. -u < xa n}";
-by (Auto_tac);
+by Auto_tac;
 qed "lemma_free4";
 
 Goal "{n. Yb n < u} Int {n. xa n = Yb n} <= {n. xa n < u}";
-by (Auto_tac);
+by Auto_tac;
 qed "lemma_free5";
 
 Goalw [Infinitesimal_def] 
diff -r a9f6994fb906 -r 351ba950d4d9 src/HOL/Real/Hyperreal/SEQ.ML
--- a/src/HOL/Real/Hyperreal/SEQ.ML	Wed Dec 20 12:14:50 2000 +0100
+++ b/src/HOL/Real/Hyperreal/SEQ.ML	Wed Dec 20 12:15:52 2000 +0100
@@ -292,17 +292,16 @@
     LIMSEQ_NSLIMSEQ_iff]) 1);
 qed "LIMSEQ_inverse";
 
-(* trivially proved *)
-Goal "[| X ----NS> a; Y ----NS> b; b ~= #0 |] \
-\     ==> (%n. (X n) * inverse(Y n)) ----NS> a*inverse(b)";
-by (blast_tac (claset() addDs [NSLIMSEQ_inverse,NSLIMSEQ_mult]) 1);
+Goal "[| X ----NS> a;  Y ----NS> b;  b ~= #0 |] \
+\     ==> (%n. X n / Y n) ----NS> a/b";
+by (asm_full_simp_tac (simpset() addsimps [NSLIMSEQ_mult, NSLIMSEQ_inverse, 
+                                           real_divide_def]) 1);
 qed "NSLIMSEQ_mult_inverse";
 
-(* let's give a standard proof of theorem *)
-Goal "[| X ----> a; Y ----> b; b ~= #0 |] \
-\     ==> (%n. (X n) * inverse(Y n)) ----> a*inverse(b)";
-by (blast_tac (claset() addDs [LIMSEQ_inverse,LIMSEQ_mult]) 1);
-qed "LIMSEQ_mult_inverse";
+Goal "[| X ----> a;  Y ----> b;  b ~= #0 |] ==> (%n. X n / Y n) ----> a/b";
+by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_mult, LIMSEQ_inverse, 
+                                           real_divide_def]) 1);
+qed "LIMSEQ_divide";
 
 (*-----------------------------------------------
             Uniqueness of limit
@@ -1296,11 +1295,11 @@
 Goalw [NSLIMSEQ_def]
      "[| #0 <= x; x < #1 |] ==> (%n. x ^ n) ----NS> #0";
 by (auto_tac (claset() addSDs [convergent_realpow],
-    simpset() addsimps [convergent_NSconvergent_iff]));
+              simpset() addsimps [convergent_NSconvergent_iff]));
 by (forward_tac [NSconvergentD] 1);
-by (auto_tac (claset(),simpset() addsimps [NSLIMSEQ_def,
-    NSCauchy_NSconvergent_iff RS sym,NSCauchy_def,
-    starfunNat_pow]));
+by (auto_tac (claset(),
+        simpset() addsimps [NSLIMSEQ_def, NSCauchy_NSconvergent_iff RS sym,
+                            NSCauchy_def, starfunNat_pow]));
 by (forward_tac [HNatInfinite_add_one] 1);
 by (dtac bspec 1 THEN assume_tac 1);
 by (dtac bspec 1 THEN assume_tac 1);
@@ -1308,17 +1307,25 @@
 by (asm_full_simp_tac (simpset() addsimps [hyperpow_add]) 1);
 by (dtac inf_close_mult_subst_SReal 1 THEN assume_tac 1);
 by (dtac inf_close_trans3 1 THEN assume_tac 1);
-by (auto_tac (claset() addSDs [rename_numerals 
-                                (real_not_refl2 RS real_mult_eq_self_zero2)], 
-    simpset() addsimps [hypreal_of_real_mult RS sym]));
+by (auto_tac (claset(),
+              simpset() addsimps [hypreal_of_real_mult RS sym]));
 qed "NSLIMSEQ_realpow_zero";
 
 (*---------------  standard version ---------------*)
 Goal "[| #0 <= x; x < #1 |] ==> (%n. x ^ n) ----> #0";
-by (asm_full_simp_tac (simpset() addsimps [NSLIMSEQ_realpow_zero,
-    LIMSEQ_NSLIMSEQ_iff]) 1);
+by (asm_simp_tac (simpset() addsimps [NSLIMSEQ_realpow_zero,
+                                      LIMSEQ_NSLIMSEQ_iff]) 1);
 qed "LIMSEQ_realpow_zero";
 
+Goal "#1 < x ==> (%n. a / (x ^ n)) ----> #0";
+by (cut_inst_tac [("a","a"),("x1","inverse x")] 
+    ([LIMSEQ_const, LIMSEQ_realpow_zero] MRS LIMSEQ_mult) 1);
+by (auto_tac (claset(), 
+              simpset() addsimps [real_divide_def, realpow_inverse])); 
+by (asm_simp_tac (simpset() addsimps [real_inverse_eq_divide,
+                                      pos_real_divide_less_eq]) 1); 
+qed "LIMSEQ_divide_realpow_zero";
+
 (*----------------------------------------------------------------
                Limit of c^n for |c| < 1  
  ---------------------------------------------------------------*)
@@ -1334,7 +1341,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 RS sym]));
 qed "LIMSEQ_rabs_realpow_zero2";
 
 Goal "abs(c) < #1 ==> (%n. c ^ n) ----NS> #0";
diff -r a9f6994fb906 -r 351ba950d4d9 src/HOL/Real/Hyperreal/Series.ML
--- a/src/HOL/Real/Hyperreal/Series.ML	Wed Dec 20 12:14:50 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Series.ML	Wed Dec 20 12:15:52 2000 +0100
@@ -99,19 +99,12 @@
 by (Auto_tac);
 qed "sumr_shift_bounds";
 
-(*FIXME: replace*)
-Goal "sumr 0 (n + n) (%i. (- #1) ^ Suc i) = #0";
+Goal "sumr 0 (#2*n) (%i. (#-1) ^ Suc i) = #0";
 by (induct_tac "n" 1);
 by (Auto_tac);
 qed "sumr_minus_one_realpow_zero";
 Addsimps [sumr_minus_one_realpow_zero];
 
-Goal "sumr 0 (n + n) (%i. (#-1) ^ Suc i) = #0";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed "sumr_minus_one_realpow_zero2";
-Addsimps [sumr_minus_one_realpow_zero2];
-
 Goal "m < Suc n ==> Suc n - m = Suc (n - m)";
 by (dtac less_imp_Suc_add 1);
 by (Auto_tac);
@@ -421,15 +414,13 @@
 (*-------------------------------------------------------------------
                     sum of geometric progression                 
  -------------------------------------------------------------------*)
-(* lemma *)
 
 Goal "x ~= #1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - #1) * inverse(x - #1)";
 by (induct_tac "n" 1);
 by (Auto_tac);
 by (res_inst_tac [("c1","x - #1")] (real_mult_right_cancel RS iffD1) 1);
 by (auto_tac (claset(),
-       simpset() addsimps [real_eq_minus_iff2 RS sym,
-                           real_mult_assoc, real_add_mult_distrib]));
+       simpset() addsimps [real_mult_assoc, real_add_mult_distrib]));
 by (auto_tac (claset(),
        simpset() addsimps [real_add_mult_distrib2,
                            real_diff_def, real_mult_commute]));
diff -r a9f6994fb906 -r 351ba950d4d9 src/HOL/Real/RealArith.ML
--- a/src/HOL/Real/RealArith.ML	Wed Dec 20 12:14:50 2000 +0100
+++ b/src/HOL/Real/RealArith.ML	Wed Dec 20 12:15:52 2000 +0100
@@ -212,11 +212,12 @@
   val dest_coeff	= dest_coeff 1
   val trans_tac         = trans_tac
   val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_plus_1s))
-            THEN ALLGOALS
-                 (simp_tac 
-                  (HOL_ss addsimps [eq_real_number_of, 
-                                    real_mult_minus_right RS sym]@
-    [mult_real_number_of, real_mult_number_of_left]@bin_simps@real_mult_ac))
+     THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@real_mult_minus_simps))
+     THEN ALLGOALS
+	  (simp_tac 
+	   (HOL_ss addsimps [eq_real_number_of, mult_real_number_of, 
+                             real_mult_number_of_left]@
+           real_minus_from_mult_simps @ real_mult_ac))
   val numeral_simp_tac	= 
          ALLGOALS (simp_tac (HOL_ss addsimps rel_real_number_of@bin_simps))
   val simplify_meta_eq  = simplify_meta_eq
@@ -260,16 +261,16 @@
 
 val real_cancel_numeral_factors = 
   map prep_simproc
-   [("realeq_cancel_numeral_factors",
+   [("realeq_cancel_numeral_factor",
      prep_pats ["(l::real) * m = n", "(l::real) = m * n"], 
      EqCancelNumeralFactor.proc),
-    ("realless_cancel_numeral_factors", 
+    ("realless_cancel_numeral_factor", 
      prep_pats ["(l::real) * m < n", "(l::real) < m * n"], 
      LessCancelNumeralFactor.proc),
-    ("realle_cancel_numeral_factors", 
+    ("realle_cancel_numeral_factor", 
      prep_pats ["(l::real) * m <= n", "(l::real) <= m * n"], 
      LeCancelNumeralFactor.proc),
-    ("realdiv_cancel_numeral_factors", 
+    ("realdiv_cancel_numeral_factor", 
      prep_pats ["((l::real) * m) / n", "(l::real) / (m * n)"], 
      DivCancelNumeralFactor.proc)];
 
diff -r a9f6994fb906 -r 351ba950d4d9 src/HOL/Real/RealBin.ML
--- a/src/HOL/Real/RealBin.ML	Wed Dec 20 12:14:50 2000 +0100
+++ b/src/HOL/Real/RealBin.ML	Wed Dec 20 12:15:52 2000 +0100
@@ -137,7 +137,7 @@
 	   real_mult_minus_1_right, real_mult_minus_1, real_inverse_1,
 	   real_minus_zero_less_iff]);
 
-AddIffs (map rename_numerals [real_mult_is_0, real_0_is_mult]);
+AddIffs (map rename_numerals [real_mult_is_0]);
 
 bind_thm ("real_0_less_mult_iff", 
 	  rename_numerals real_zero_less_mult_iff);
diff -r a9f6994fb906 -r 351ba950d4d9 src/HOL/Real/RealDef.ML
--- a/src/HOL/Real/RealDef.ML	Wed Dec 20 12:14:50 2000 +0100
+++ b/src/HOL/Real/RealDef.ML	Wed Dec 20 12:15:52 2000 +0100
@@ -270,20 +270,6 @@
 by (simp_tac (simpset() addsimps [real_add_commute,real_add_left_cancel]) 1);
 qed "real_add_right_cancel";
 
-Goal "((x::real) = y) = (0 = x + (- y))";
-by (Step_tac 1);
-by (res_inst_tac [("x1","-y")] 
-      (real_add_right_cancel RS iffD1) 2);
-by Auto_tac;
-qed "real_eq_minus_iff"; 
-
-Goal "((x::real) = y) = (x + (- y) = 0)";
-by (Step_tac 1);
-by (res_inst_tac [("x1","-y")] 
-      (real_add_right_cancel RS iffD1) 2);
-by Auto_tac;
-qed "real_eq_minus_iff2"; 
-
 Goal "(0::real) - x = -x";
 by (simp_tac (simpset() addsimps [real_diff_def]) 1);
 qed "real_diff_0";
diff -r a9f6994fb906 -r 351ba950d4d9 src/HOL/Real/RealOrd.ML
--- a/src/HOL/Real/RealOrd.ML	Wed Dec 20 12:14:50 2000 +0100
+++ b/src/HOL/Real/RealOrd.ML	Wed Dec 20 12:15:52 2000 +0100
@@ -698,26 +698,7 @@
 by Auto_tac;
 by (blast_tac (claset() addIs [ccontr] addDs [real_mult_not_zero]) 1);
 qed "real_mult_is_0";
-
-Goal "(0 = x*y) = (0 = x | (0::real) = y)";
-by (stac eq_commute 1 THEN stac real_mult_is_0 1);
-by Auto_tac;
-qed "real_0_is_mult";
-AddIffs [real_mult_is_0, real_0_is_mult];
-
-Goal "[| x ~= 1r; y * x = y |] ==> y = 0";
-by (subgoal_tac "y*(1r + -x) = 0" 1);
-by (stac real_add_mult_distrib2 2);
-by (auto_tac (claset(),
-	      simpset() addsimps [real_eq_minus_iff2 RS sym]));
-qed "real_mult_eq_self_zero";
-Addsimps [real_mult_eq_self_zero];
-
-Goal "[| x ~= 1r; y = y * x |] ==> y = 0";
-by (dtac sym 1);
-by (Asm_full_simp_tac 1);
-qed "real_mult_eq_self_zero2";
-Addsimps [real_mult_eq_self_zero2];
+AddIffs [real_mult_is_0];
 
 Goal "[| 0 <= x * y; 0 < x |] ==> (0::real) <= y";
 by (ftac real_inverse_gt_zero 1);
diff -r a9f6994fb906 -r 351ba950d4d9 src/HOL/Real/RealPow.ML
--- a/src/HOL/Real/RealPow.ML	Wed Dec 20 12:14:50 2000 +0100
+++ b/src/HOL/Real/RealPow.ML	Wed Dec 20 12:15:52 2000 +0100
@@ -43,7 +43,7 @@
 qed "realpow_one";
 Addsimps [realpow_one];
 
-Goal "(r::real) ^ 2 = r * r";
+Goal "(r::real)^2 = r * r";
 by (Simp_tac 1);
 qed "realpow_two";
 
@@ -111,24 +111,24 @@
 by (auto_tac (claset(),simpset() addsimps real_mult_ac));
 qed "realpow_mult";
 
-Goal "(#0::real) <= r ^ 2";
+Goal "(#0::real) <= r^2";
 by (simp_tac (simpset() addsimps [rename_numerals real_le_square]) 1);
 qed "realpow_two_le";
 Addsimps [realpow_two_le];
 
-Goal "abs((x::real) ^ 2) = x ^ 2";
+Goal "abs((x::real)^2) = x^2";
 by (simp_tac (simpset() addsimps [abs_eqI1, 
 				  rename_numerals real_le_square]) 1);
 qed "abs_realpow_two";
 Addsimps [abs_realpow_two];
 
-Goal "abs(x::real) ^ 2 = x ^ 2";
+Goal "abs(x::real) ^ 2 = x^2";
 by (simp_tac (simpset() addsimps [realpow_abs,abs_eqI1]
                         delsimps [realpow_Suc]) 1);
 qed "realpow_two_abs";
 Addsimps [realpow_two_abs];
 
-Goal "(#1::real) < r ==> #1 < r ^ 2";
+Goal "(#1::real) < r ==> #1 < r^2";
 by Auto_tac;
 by (cut_facts_tac [rename_numerals real_zero_less_one] 1);
 by (forw_inst_tac [("R1.0","#0")] real_less_trans 1);
@@ -352,37 +352,27 @@
 Addsimps [realpow_two_mult_inverse];
 
 (* 05/00 *)
-Goal "(-x) ^ 2 = (x::real) ^ 2";
+Goal "(-x)^2 = (x::real) ^ 2";
 by (Simp_tac 1);
 qed "realpow_two_minus";
 Addsimps [realpow_two_minus];
 
-Goal "(x::real) ^ 2 + - (y ^ 2) = (x + -y) * (x + y)";
-by (simp_tac (simpset() addsimps [real_add_mult_distrib2,
-    real_add_mult_distrib, real_minus_mult_eq2 RS sym] 
-    @ real_mult_ac) 1);
-qed "realpow_two_add_minus";
-
-Goalw [real_diff_def] 
-      "(x::real) ^ 2 - y ^ 2 = (x - y) * (x + y)";
-by (simp_tac (simpset() addsimps [realpow_two_add_minus]
-                        delsimps [realpow_Suc]) 1);
+Goalw [real_diff_def] "(x::real)^2 - y^2 = (x - y) * (x + y)";
+by (simp_tac (simpset() addsimps 
+              [real_add_mult_distrib2, real_add_mult_distrib, 
+               real_minus_mult_eq2 RS sym] @ real_mult_ac) 1);
 qed "realpow_two_diff";
 
-Goalw [real_diff_def] 
-      "((x::real) ^ 2 = y ^ 2) = (x = y | x = -y)";
-by (auto_tac (claset(),simpset() delsimps [realpow_Suc]));
-by (dtac (rename_numerals (real_eq_minus_iff RS iffD1 RS sym)) 1);
-by (auto_tac (claset() addDs [rename_numerals real_add_minus_eq_minus], 
-          simpset() addsimps [realpow_two_add_minus] delsimps [realpow_Suc]));
+Goalw [real_diff_def] "((x::real)^2 = y^2) = (x = y | x = -y)";
+by (cut_inst_tac [("x","x"),("y","y")] realpow_two_diff 1);
+by (auto_tac (claset(), simpset() delsimps [realpow_Suc]));
 qed "realpow_two_disj";
 
 (* used in Transc *)
 Goal  "[|(x::real) ~= #0; m <= n |] ==> x ^ (n - m) = x ^ n * inverse (x ^ m)";
 by (auto_tac (claset(),
-              simpset() addsimps [le_eq_less_or_eq,
-                                  less_iff_Suc_add,realpow_add,
-                                  realpow_not_zero] @ real_mult_ac));
+       simpset() addsimps [le_eq_less_or_eq, less_iff_Suc_add, realpow_add,
+                           realpow_not_zero] @ real_mult_ac));
 qed "realpow_diff";
 
 Goal "real_of_nat (m) ^ n = real_of_nat (m ^ n)";