# HG changeset patch
# User paulson
# Date 977390193 -3600
# Node ID c838477b5c18b02bfde77b639f8903f6af047dd3
# Parent  07f75bf77a332e5cadcb703f91b194568155105c
more tidying, especially to rationalize the simprules

diff -r 07f75bf77a33 -r c838477b5c18 src/HOL/Real/Hyperreal/HRealAbs.ML
--- a/src/HOL/Real/Hyperreal/HRealAbs.ML	Thu Dec 21 10:16:07 2000 +0100
+++ b/src/HOL/Real/Hyperreal/HRealAbs.ML	Thu Dec 21 10:16:33 2000 +0100
@@ -5,17 +5,16 @@
                   Similar to RealAbs.thy
 *) 
 
-
 (*------------------------------------------------------------
   absolute value on hyperreals as pointwise operation on 
   equivalence class representative
  ------------------------------------------------------------*)
 
 Goalw [hrabs_def]
-"abs (Abs_hypreal (hyprel ^^ {X})) = \
-\            Abs_hypreal(hyprel ^^ {%n. abs (X n)})";
-by (auto_tac (claset(),simpset() addsimps [hypreal_zero_def,
-    hypreal_le,hypreal_minus]));
+     "abs (Abs_hypreal (hyprel ^^ {X})) = \
+\     Abs_hypreal(hyprel ^^ {%n. abs (X n)})";
+by (auto_tac (claset(),
+           simpset() addsimps [hypreal_zero_def, hypreal_le,hypreal_minus]));
 by (ALLGOALS(Ultra_tac THEN' arith_tac ));
 qed "hypreal_hrabs";
 
@@ -23,49 +22,38 @@
    Properties of the absolute value function over the reals
    (adapted version of previously proved theorems about abs)
  ------------------------------------------------------------*)
-Goalw [hrabs_def] "abs r = (if (0::hypreal)<=r then r else -r)";
-by (Step_tac 1);
-qed "hrabs_iff";
 
-Goalw [hrabs_def] "abs (0::hypreal) = (0::hypreal)";
-by (rtac (hypreal_le_refl RS if_P) 1);
+Goal "abs (0::hypreal) = 0";
+by (simp_tac (simpset() addsimps [hrabs_def]) 1); 
 qed "hrabs_zero";
-
 Addsimps [hrabs_zero];
 
-Goalw [hrabs_def] "abs (0::hypreal) = -(0::hypreal)";
-by (rtac (hypreal_minus_zero RS ssubst) 1);
-by (rtac if_cancel 1);
-qed "hrabs_minus_zero";
-
-val [prem] = goalw thy [hrabs_def] "(0::hypreal)<=x ==> abs x = x";
-by (rtac (prem RS if_P) 1);
+Goal "(0::hypreal)<=x ==> abs x = x";
+by (asm_simp_tac (simpset() addsimps [hrabs_def]) 1); 
 qed "hrabs_eqI1";
 
-val [prem] = goalw thy [hrabs_def] "(0::hypreal)<x ==> abs x = x";
-by (simp_tac (simpset() addsimps [(prem 
-    RS hypreal_less_imp_le),hrabs_eqI1]) 1);
+Goal "(0::hypreal)<x ==> abs x = x";
+by (asm_simp_tac (simpset() addsimps [hypreal_less_imp_le, hrabs_eqI1]) 1);
 qed "hrabs_eqI2";
 
-val [prem] = goalw thy [hrabs_def,hypreal_le_def] 
-    "x<(0::hypreal) ==> abs x = -x";
-by (simp_tac (simpset() addsimps [prem,if_not_P]) 1);
+Goal "x<(0::hypreal) ==> abs x = -x";
+by (asm_simp_tac (simpset() addsimps [hypreal_le_def, hrabs_def]) 1); 
 qed "hrabs_minus_eqI2";
 
-Goal "!!x. x<=(0::hypreal) ==> abs x = -x";
-by (dtac hypreal_le_imp_less_or_eq 1);
-by (fast_tac (HOL_cs addIs [hrabs_minus_zero,
-    hrabs_minus_eqI2]) 1);
+Goal "x<=(0::hypreal) ==> abs x = -x";
+by (auto_tac (claset() addDs [order_antisym], simpset() addsimps [hrabs_def])); 
 qed "hrabs_minus_eqI1";
 
-Goalw [hrabs_def,hypreal_le_def] "(0::hypreal)<= abs x";
-by (auto_tac (claset() addDs [hypreal_minus_zero_less_iff RS iffD2,
-    hypreal_less_asym],simpset()));
+Goal "(0::hypreal)<= abs x";
+by (auto_tac (claset() addDs [hypreal_minus_zero_less_iff RS iffD2, 
+                              hypreal_less_asym], 
+              simpset() addsimps [hypreal_le_def, hrabs_def]));
 qed "hrabs_ge_zero";
 
 Goal "abs(abs x) = abs (x::hypreal)";
-by (res_inst_tac [("r1","abs x")] (hrabs_iff RS ssubst) 1);
-by (blast_tac (claset() addIs [if_P,hrabs_ge_zero]) 1);
+by (auto_tac (claset() addDs [hypreal_minus_zero_less_iff RS iffD2, 
+                              hypreal_less_asym], 
+              simpset() addsimps [hypreal_le_def, hrabs_def]));
 qed "hrabs_idempotent";
 Addsimps [hrabs_idempotent];
 
@@ -87,8 +75,8 @@
 Goal "abs(x*(y::hypreal)) = (abs x)*(abs y)";
 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_hrabs,
-    hypreal_mult,abs_mult]));
+by (auto_tac (claset(), 
+              simpset() addsimps [hypreal_hrabs, hypreal_mult,abs_mult]));
 qed "hrabs_mult";
 
 Goal "abs(inverse(x)) = inverse(abs(x::hypreal))";
@@ -103,31 +91,23 @@
 Goal "abs(x+(y::hypreal)) <= abs x + abs y";
 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_hrabs,
-    hypreal_add,hypreal_le,abs_triangle_ineq]));
+by (auto_tac (claset(), 
+      simpset() addsimps [hypreal_hrabs, hypreal_add,hypreal_le,
+                        abs_triangle_ineq]));
 qed "hrabs_triangle_ineq";
 
 Goal "abs((w::hypreal) + x + y) <= abs(w) + abs(x) + abs(y)";
-by (auto_tac (claset() addSIs [(hrabs_triangle_ineq 
-    RS hypreal_le_trans),hypreal_add_left_le_mono1],
+by (auto_tac (claset() addSIs [hrabs_triangle_ineq RS hypreal_le_trans,
+                               hypreal_add_left_le_mono1],
     simpset() addsimps [hypreal_add_assoc]));
 qed "hrabs_triangle_ineq_three";
 
 Goalw [hrabs_def] "abs(-x)=abs((x::hypreal))";
-by (auto_tac (claset() addSDs [not_hypreal_leE,
-   hypreal_less_asym] addIs [hypreal_le_anti_sym],
-   simpset() addsimps [hypreal_ge_zero_iff]));
+by (auto_tac (claset() addSDs [not_hypreal_leE, hypreal_less_asym] 
+                       addIs [hypreal_le_anti_sym],
+              simpset() addsimps [hypreal_ge_zero_iff]));
 qed "hrabs_minus_cancel";
-
-Goal "abs((x::hypreal) + -y) = abs (y + -x)";
-by (rtac (hrabs_minus_cancel RS subst) 1);
-by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
-qed "hrabs_minus_add_cancel";
-
-Goal "abs((x::hypreal) + -y) <= abs x + abs y";
-by (res_inst_tac [("x1","y")] (hrabs_minus_cancel RS subst) 1);
-by (rtac hrabs_triangle_ineq 1);
-qed "rhabs_triangle_minus_ineq";
+Addsimps [hrabs_minus_cancel];
 
 val prem1::prem2::rest = goal thy 
     "[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)";
@@ -136,13 +116,6 @@
 by (rtac ([prem1,prem2] MRS hypreal_add_less_mono) 1);
 qed "hrabs_add_less";
 
-Goal "[| abs x < r; abs y < s |] \
-\     ==> abs(x+ -y) < r + (s::hypreal)";
-by (rotate_tac 1 1);
-by (dtac (hrabs_minus_cancel RS ssubst) 1);
-by (asm_simp_tac (simpset() addsimps [hrabs_add_less]) 1);
-qed "hrabs_add_minus_less";
-
 val prem1::prem2::rest = 
     goal thy "[| abs x<r; abs y<s |] ==> abs(x*y)<r*(s::hypreal)";
 by (simp_tac (simpset() addsimps [hrabs_mult]) 1);
@@ -153,11 +126,11 @@
 by (rtac (prem2 RS (hrabs_ge_zero RS hypreal_le_less_trans)) 1);
 by (rtac prem1 1);
 by (rtac ([prem1 RS (hrabs_ge_zero RS hypreal_le_less_trans),
-   prem2 RS (hrabs_ge_zero RS hypreal_le_less_trans)] 
-   MRS hypreal_mult_order) 1);
+           prem2 RS (hrabs_ge_zero RS hypreal_le_less_trans)] 
+          MRS hypreal_mult_order) 1);
 qed "hrabs_mult_less";
 
-Goal "!! x y r. 1hr < abs x ==> abs y <= abs(x*y)";
+Goal "1hr < abs x ==> abs y <= abs(x*y)";
 by (cut_inst_tac [("x1","y")] (hrabs_ge_zero RS hypreal_le_imp_less_or_eq) 1);
 by (EVERY1[etac disjE,rtac hypreal_less_imp_le]);
 by (dres_inst_tac [("x1","1hr")]  (hypreal_less_minus_iff RS iffD1) 1);
@@ -170,30 +143,24 @@
 by (asm_full_simp_tac (simpset() addsimps [hypreal_le_refl,hrabs_mult]) 1);
 qed "hrabs_mult_le";
 
-Goal "!!x. [| 1hr < abs x; r < abs y|] ==> r < abs(x*y)";
+Goal "[| 1hr < abs x; r < abs y|] ==> r < abs(x*y)";
 by (fast_tac (HOL_cs addIs [hrabs_mult_le, hypreal_less_le_trans]) 1);
 qed "hrabs_mult_gt";
 
-Goal "!!r. abs x < r ==> (0::hypreal) < r";
+Goal "abs x < r ==> (0::hypreal) < r";
 by (blast_tac (claset() addSIs [hypreal_le_less_trans,
     hrabs_ge_zero]) 1);
 qed "hrabs_less_gt_zero";
 
 Goalw [hrabs_def] "abs 1hr = 1hr";
-by (auto_tac (claset() addSDs [not_hypreal_leE 
-    RS hypreal_less_asym],simpset() addsimps 
-    [hypreal_zero_less_one]));
+by (auto_tac (claset() addSDs [not_hypreal_leE RS hypreal_less_asym], 
+      simpset() addsimps [hypreal_zero_less_one]));
 qed "hrabs_one";
 
-val prem1::prem2::rest = 
-    goal thy "[| (0::hypreal) < x ; x < r |] ==> abs x < r";
-by (simp_tac (simpset() addsimps [(prem1 RS hrabs_eqI2),prem2]) 1);
-qed "hrabs_lessI";
-
 Goal "abs x = (x::hypreal) | abs x = -x";
 by (cut_inst_tac [("x","0"),("y","x")] hypreal_linear 1);
 by (fast_tac (claset() addIs [hrabs_eqI2,hrabs_minus_eqI2,
-                            hrabs_zero,hrabs_minus_zero]) 1);
+                            hrabs_zero]) 1);
 qed "hrabs_disj";
 
 Goal "abs x = (y::hypreal) ==> x = y | -x = y";
@@ -217,54 +184,28 @@
 qed "hrabs_interval_iff";
 
 Goal "(abs x < (r::hypreal)) = (- x < r & x < r)";
-by (auto_tac (claset(),simpset() addsimps [hrabs_interval_iff]));
+by (auto_tac (claset(),  simpset() addsimps [hrabs_interval_iff]));
 by (dtac (hypreal_less_swap_iff RS iffD1) 1);
 by (dtac (hypreal_less_swap_iff RS iffD1) 2);
 by (Auto_tac);
 qed "hrabs_interval_iff2";
 
-Goal 
-     "(abs (x + -y) < (r::hypreal)) = (y + -r < x & x < y + r)";
-by (auto_tac (claset(),simpset() addsimps 
-     [hrabs_interval_iff]));
-by (ALLGOALS(dtac (hypreal_less_minus_iff RS iffD1)));
-by (ALLGOALS(dtac (hypreal_less_minus_iff RS iffD1)));
-by (ALLGOALS(rtac (hypreal_less_minus_iff RS iffD2)));
-by (auto_tac (claset(),simpset() addsimps 
-    [hypreal_minus_add_distrib] addsimps hypreal_add_ac));
-qed "hrabs_add_minus_interval_iff";
-
-Goal "x < (y::hypreal) ==> abs(y + -x) = y + -x";
-by (dtac (hypreal_less_minus_iff RS iffD1) 1);
-by (etac hrabs_eqI2 1);
-qed "hrabs_less_eqI2";
-
-Goal "x < (y::hypreal) ==> abs(x + -y) = y + -x";
-by (auto_tac (claset() addDs [hrabs_less_eqI2],
-              simpset() addsimps [hrabs_minus_add_cancel]));
-qed "hrabs_less_eqI2a";
-
-Goal "x <= (y::hypreal) ==> abs(y + -x) = y + -x";
-by (auto_tac (claset() addDs  [hypreal_le_imp_less_or_eq,
-              hrabs_less_eqI2],simpset()));
-qed "hrabs_le_eqI2";
-
-Goal "x <= (y::hypreal) ==> abs(x + -y) = y + -x";
-by (auto_tac (claset() addDs [hrabs_le_eqI2],
-              simpset() addsimps [hrabs_minus_add_cancel]));
-qed "hrabs_le_eqI2a";
-
 (* Needed in Geom.ML *)
-Goal "(y::hypreal) + - x + (y + - z) = abs (x + - z) \
-\     ==> y = z | x = y";
+Goal "(y::hypreal) + - x + (y + - z) = abs (x + - z) ==> y = z | x = y";
 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_hrabs,
-    hypreal_minus,hypreal_add]));
+by (auto_tac (claset(), 
+              simpset() addsimps [hypreal_hrabs, hypreal_minus,hypreal_add]));
 by (Ultra_tac 1 THEN arith_tac 1);
 qed "hrabs_add_lemma_disj";
 
+(***SHOULD BE TRIVIAL GIVEN SIMPROCS
+Goal "abs((x::hypreal) + -y) = abs (y + -x)";
+by (rtac (hrabs_minus_cancel RS subst) 1);
+by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
+qed "hrabs_minus_add_cancel";
+
 (* Needed in Geom.ML *)
 Goal "(x::hypreal) + - y + (z + - y) = abs (x + - z) \
 \     ==> y = z | x = y";
@@ -274,11 +215,12 @@
 by (asm_full_simp_tac (simpset() addsimps [hrabs_minus_add_cancel] 
          @ hypreal_add_ac) 1);
 qed "hrabs_add_lemma_disj2";
+***)
  
 (*----------------------------------------------------------
     Relating hrabs to abs through embedding of IR into IR*
  ----------------------------------------------------------*)
 Goalw [hypreal_of_real_def] 
     "abs (hypreal_of_real r) = hypreal_of_real (abs r)";
-by (auto_tac (claset(),simpset() addsimps [hypreal_hrabs]));
+by (auto_tac (claset(), simpset() addsimps [hypreal_hrabs]));
 qed "hypreal_of_real_hrabs";
diff -r 07f75bf77a33 -r c838477b5c18 src/HOL/Real/Hyperreal/HyperDef.ML
--- a/src/HOL/Real/Hyperreal/HyperDef.ML	Thu Dec 21 10:16:07 2000 +0100
+++ b/src/HOL/Real/Hyperreal/HyperDef.ML	Thu Dec 21 10:16:33 2000 +0100
@@ -707,11 +707,9 @@
               simpset()));
 qed "hypreal_mult_zero_disj";
 
-Goal "x ~= 0 ==> x * x ~= (0::hypreal)";
-by (blast_tac (claset() addDs [hypreal_mult_not_0]) 1);
-qed "hypreal_mult_self_not_zero";
-
-Goal "[| x ~= 0; y ~= 0 |] ==> inverse(x*y) = inverse(x)*inverse(y::hypreal)";
+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]));
@@ -1109,6 +1107,7 @@
 Goalw [hypreal_of_real_def] "hypreal_of_real (-r) = - hypreal_of_real  r";
 by (auto_tac (claset(),simpset() addsimps [hypreal_minus]));
 qed "hypreal_of_real_minus";
+Addsimps [hypreal_of_real_minus];
 
 (*DON'T insert this or the next one as default simprules.
   They are used in both orientations and anyway aren't the ones we finally
diff -r 07f75bf77a33 -r c838477b5c18 src/HOL/Real/Hyperreal/HyperPow.ML
--- a/src/HOL/Real/Hyperreal/HyperPow.ML	Thu Dec 21 10:16:07 2000 +0100
+++ b/src/HOL/Real/Hyperreal/HyperPow.ML	Thu Dec 21 10:16:33 2000 +0100
@@ -20,18 +20,17 @@
 by (induct_tac "n" 1);
 by (Auto_tac);
 by (forw_inst_tac [("n","n")] hrealpow_not_zero 1);
-by (auto_tac (claset() addDs [inverse_mult_eq],
-    simpset()));
+by (auto_tac (claset(), simpset() addsimps [inverse_mult_eq]));
 qed_spec_mp "hrealpow_inverse";
 
 Goal "abs (r::hypreal) ^ n = abs (r ^ n)";
 by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps [hrabs_mult,hrabs_one]));
+by (auto_tac (claset(), simpset() addsimps [hrabs_mult,hrabs_one]));
 qed "hrealpow_hrabs";
 
 Goal "(r::hypreal) ^ (n + m) = (r ^ n) * (r ^ m)";
 by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps hypreal_mult_ac));
+by (auto_tac (claset(), simpset() addsimps hypreal_mult_ac));
 qed "hrealpow_add";
 
 Goal "(r::hypreal) ^ 1 = r";
@@ -46,33 +45,34 @@
 Goal "(0::hypreal) < r --> 0 <= r ^ n";
 by (induct_tac "n" 1);
 by (auto_tac (claset() addDs [hypreal_less_imp_le] 
-    addIs [hypreal_le_mult_order],simpset() addsimps 
-    [hypreal_zero_less_one RS hypreal_less_imp_le]));
+                       addIs [hypreal_le_mult_order],
+             simpset() addsimps [hypreal_zero_less_one RS hypreal_less_imp_le]));
 qed_spec_mp "hrealpow_ge_zero";
 
 Goal "(0::hypreal) < r --> 0 < r ^ n";
 by (induct_tac "n" 1);
 by (auto_tac (claset() addIs [hypreal_mult_order],
-    simpset() addsimps [hypreal_zero_less_one]));
+              simpset() addsimps [hypreal_zero_less_one]));
 qed_spec_mp "hrealpow_gt_zero";
 
 Goal "(0::hypreal) <= r --> 0 <= r ^ n";
 by (induct_tac "n" 1);
-by (auto_tac (claset() addIs [hypreal_le_mult_order],simpset() 
-    addsimps [hypreal_zero_less_one RS hypreal_less_imp_le]));
+by (auto_tac (claset() addIs [hypreal_le_mult_order],
+          simpset() addsimps [hypreal_zero_less_one RS hypreal_less_imp_le]));
 qed_spec_mp "hrealpow_ge_zero2";
 
 Goal "(0::hypreal) < x & x <= y --> x ^ n <= y ^ n";
 by (induct_tac "n" 1);
 by (auto_tac (claset() addSIs [hypreal_mult_le_mono],
-    simpset() addsimps [hypreal_le_refl]));
+              simpset() addsimps [hypreal_le_refl]));
 by (asm_simp_tac (simpset() addsimps [hrealpow_ge_zero]) 1);
 qed_spec_mp "hrealpow_le";
 
 Goal "(0::hypreal) < x & x < y & 0 < n --> x ^ n < y ^ n";
 by (induct_tac "n" 1);
 by (auto_tac (claset() addIs [hypreal_mult_less_mono,gr0I] 
-    addDs [hrealpow_gt_zero],simpset()));
+                       addDs [hrealpow_gt_zero],
+              simpset()));
 qed "hrealpow_less";
 
 Goal "1hr ^ n = 1hr";
@@ -82,21 +82,20 @@
 Addsimps [hrealpow_eq_one];
 
 Goal "abs(-(1hr ^ n)) = 1hr";
-by (simp_tac (simpset() addsimps 
-    [hrabs_minus_cancel,hrabs_one]) 1);
+by (simp_tac (simpset() addsimps [hrabs_one]) 1);
 qed "hrabs_minus_hrealpow_one";
 Addsimps [hrabs_minus_hrealpow_one];
 
 Goal "abs((-1hr) ^ n) = 1hr";
 by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps [hrabs_mult,
-         hrabs_minus_cancel,hrabs_one]));
+by (auto_tac (claset(),
+      simpset() addsimps [hrabs_mult, hrabs_one]));
 qed "hrabs_hrealpow_minus_one";
 Addsimps [hrabs_hrealpow_minus_one];
 
 Goal "((r::hypreal) * s) ^ n = (r ^ n) * (s ^ n)";
 by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps hypreal_mult_ac));
+by (auto_tac (claset(), simpset() addsimps hypreal_mult_ac));
 qed "hrealpow_mult";
 
 Goal "(0::hypreal) <= r ^ 2";
@@ -105,12 +104,12 @@
 Addsimps [hrealpow_two_le];
 
 Goal "(0::hypreal) <= u ^ 2 + v ^ 2";
-by (auto_tac (claset() addIs [hypreal_le_add_order],simpset()));
+by (auto_tac (claset() addIs [hypreal_le_add_order], simpset()));
 qed "hrealpow_two_le_add_order";
 Addsimps [hrealpow_two_le_add_order];
 
 Goal "(0::hypreal) <= u ^ 2 + v ^ 2 + w ^ 2";
-by (auto_tac (claset() addSIs [hypreal_le_add_order],simpset()));
+by (auto_tac (claset() addSIs [hypreal_le_add_order], simpset()));
 qed "hrealpow_two_le_add_order2";
 Addsimps [hrealpow_two_le_add_order2];
 
@@ -132,12 +131,12 @@
 Addsimps [hrealpow_two_hrabs];
 
 Goal "!!r. 1hr < r ==> 1hr < r ^ 2";
-by (auto_tac (claset(),simpset() addsimps [hrealpow_two]));
+by (auto_tac (claset(), simpset() addsimps [hrealpow_two]));
 by (cut_facts_tac [hypreal_zero_less_one] 1);
 by (forw_inst_tac [("R1.0","0")] hypreal_less_trans 1);
 by (assume_tac 1);
 by (dres_inst_tac [("z","r"),("x","1hr")] hypreal_mult_less_mono1 1);
-by (auto_tac (claset() addIs [hypreal_less_trans],simpset()));
+by (auto_tac (claset() addIs [hypreal_less_trans], simpset()));
 qed "hrealpow_two_gt_one";
 
 Goal "!!r. 1hr <= r ==> 1hr <= r ^ 2";
@@ -151,7 +150,8 @@
 by (forw_inst_tac [("n1","n")]
     ((hypreal_not_refl2 RS not_sym) RS hrealpow_not_zero RS not_sym) 1);
 by (auto_tac (claset() addSDs [hypreal_le_imp_less_or_eq]
-     addIs [hypreal_mult_order],simpset()));
+                       addIs [hypreal_mult_order],
+              simpset()));
 qed "hrealpow_Suc_gt_zero";
 
 Goal "!!r. (0::hypreal) <= r ==> 0 <= r ^ Suc n";
@@ -170,8 +170,9 @@
 
 Goal "hypreal_of_nat n < (1hr + 1hr) ^ n";
 by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_of_nat_Suc,hypreal_of_nat_zero,
-    hypreal_zero_less_one,hypreal_add_mult_distrib,hypreal_of_nat_one]));
+by (auto_tac (claset(),
+        simpset() addsimps [hypreal_of_nat_Suc,hypreal_of_nat_zero,
+          hypreal_zero_less_one,hypreal_add_mult_distrib,hypreal_of_nat_one]));
 by (blast_tac (claset() addSIs [hypreal_add_less_le_mono,
     two_hrealpow_ge_one]) 1);
 qed "two_hrealpow_gt";
@@ -195,21 +196,21 @@
 
 Goal "(0::hypreal) < r & r < 1hr --> r ^ Suc n < r ^ n";
 by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps 
-        [hypreal_mult_less_mono2]));
+by (auto_tac (claset(),
+              simpset() addsimps [hypreal_mult_less_mono2]));
 qed_spec_mp "hrealpow_Suc_less";
 
 Goal "(0::hypreal) <= r & r < 1hr --> r ^ Suc n <= r ^ n";
 by (induct_tac "n" 1);
-by (auto_tac (claset() addIs [hypreal_less_imp_le] addSDs
-     [hypreal_le_imp_less_or_eq,hrealpow_Suc_less],simpset()
-     addsimps [hypreal_le_refl,hypreal_mult_less_mono2]));
+by (auto_tac (claset() addIs [hypreal_less_imp_le]
+                       addSDs [hypreal_le_imp_less_or_eq,hrealpow_Suc_less],
+      simpset() addsimps [hypreal_le_refl,hypreal_mult_less_mono2]));
 qed_spec_mp "hrealpow_Suc_le";
 
 (* a few more theorems needed here *)
 Goal "1hr <= r --> r ^ n <= r ^ Suc n";
 by (induct_tac "n" 1);
-by (auto_tac (claset() addSIs [hypreal_mult_le_le_mono1],simpset()));
+by (auto_tac (claset() addSIs [hypreal_mult_le_le_mono1], simpset()));
 by (rtac ccontr 1 THEN dtac not_hypreal_leE 1);
 by (dtac hypreal_le_less_trans 1 THEN assume_tac 1);
 by (etac (hypreal_zero_less_one RS hypreal_less_asym) 1);
@@ -217,8 +218,8 @@
 
 Goal "Abs_hypreal(hyprel^^{%n. X n}) ^ m = Abs_hypreal(hyprel^^{%n. (X n) ^ m})";
 by (nat_ind_tac "m" 1);
-by (auto_tac (claset(),simpset() addsimps 
-    [hypreal_one_def,hypreal_mult]));
+by (auto_tac (claset(),
+              simpset() addsimps [hypreal_one_def,hypreal_mult]));
 qed "hrealpow";
 
 Goal "(x + (y::hypreal)) ^ 2 = \
@@ -238,24 +239,23 @@
   "[|(0::hypreal) <= x;0 <= y;x ^ Suc n <= y ^ Suc n |] ==> x <= y";
 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps 
-    [hrealpow,hypreal_le,hypreal_mult]));
-by (ultra_tac (claset() addIs [realpow_increasing],simpset()) 1);
+by (auto_tac (claset(),
+              simpset() addsimps [hrealpow,hypreal_le,hypreal_mult]));
+by (ultra_tac (claset() addIs [realpow_increasing], simpset()) 1);
 qed "hrealpow_increasing";
 
 goalw HyperPow.thy [hypreal_zero_def] 
   "!!x. [|(0::hypreal) <= x;0 <= y;x ^ Suc n = y ^ Suc n |] ==> x = y";
 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps 
-    [hrealpow,hypreal_mult,hypreal_le]));
+by (auto_tac (claset(), simpset() addsimps [hrealpow,hypreal_mult,hypreal_le]));
 by (ultra_tac (claset() addIs [realpow_Suc_cancel_eq],
     simpset()) 1);
 qed "hrealpow_Suc_cancel_eq";
 
 Goal "x : HFinite --> x ^ n : HFinite";
 by (induct_tac "n" 1);
-by (auto_tac (claset() addIs [HFinite_mult],simpset()));
+by (auto_tac (claset() addIs [HFinite_mult], simpset()));
 qed_spec_mp "hrealpow_HFinite";
 
 (*---------------------------------------------------------------
@@ -281,8 +281,7 @@
 Goalw [hypreal_zero_def,hypnat_one_def]
       "(0::hypreal) pow (n + 1hn) = 0";
 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps 
-    [hyperpow,hypnat_add]));
+by (auto_tac (claset(), simpset() addsimps [hyperpow,hypnat_add]));
 qed "hyperpow_zero";
 Addsimps [hyperpow_zero];
 
@@ -290,7 +289,7 @@
       "r ~= (0::hypreal) --> r pow n ~= 0";
 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 [hyperpow]));
+by (auto_tac (claset(), simpset() addsimps [hyperpow]));
 by (dtac FreeUltrafilterNat_Compl_mem 1);
 by (fuf_empty_tac (claset() addIs [realpow_not_zero RS notE],
     simpset()) 1);
@@ -304,57 +303,56 @@
     simpset() addsimps [hypreal_inverse,hyperpow]));
 by (rtac FreeUltrafilterNat_subset 1);
 by (auto_tac (claset() addDs [realpow_not_zero] 
-    addIs [realpow_inverse],simpset()));
+                       addIs [realpow_inverse], 
+              simpset()));
 qed "hyperpow_inverse";
 
 Goal "abs r pow n = abs (r pow n)";
 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]));
+by (auto_tac (claset(),
+              simpset() addsimps [hypreal_hrabs, hyperpow,realpow_abs]));
 qed "hyperpow_hrabs";
 
 Goal "r pow (n + m) = (r pow n) * (r pow m)";
 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
 by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
 by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hyperpow,hypnat_add,
-     hypreal_mult,realpow_add]));
+by (auto_tac (claset(),
+          simpset() addsimps [hyperpow,hypnat_add, hypreal_mult,realpow_add]));
 qed "hyperpow_add";
 
 Goalw [hypnat_one_def] "r pow 1hn = r";
 by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hyperpow]));
+by (auto_tac (claset(), simpset() addsimps [hyperpow]));
 qed "hyperpow_one";
 Addsimps [hyperpow_one];
 
 Goalw [hypnat_one_def] 
       "r pow (1hn + 1hn) = r * r";
 by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hyperpow,hypnat_add,
-     hypreal_mult,realpow_two]));
+by (auto_tac (claset(),
+           simpset() addsimps [hyperpow,hypnat_add, hypreal_mult,realpow_two]));
 qed "hyperpow_two";
 
 Goalw [hypreal_zero_def]
       "(0::hypreal) < r --> 0 < r pow n";
 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
 by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
-by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset,
-    realpow_gt_zero],simpset() addsimps [hyperpow,hypreal_less,
-    hypreal_le]));
+by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset, realpow_gt_zero],
+       simpset() addsimps [hyperpow,hypreal_less, hypreal_le]));
 qed_spec_mp "hyperpow_gt_zero";
 
 Goal "(0::hypreal) < r --> 0 <= r pow n";
-by (blast_tac (claset() addSIs [hyperpow_gt_zero,
-    hypreal_less_imp_le]) 1);
+by (blast_tac (claset() addSIs [hyperpow_gt_zero, hypreal_less_imp_le]) 1);
 qed_spec_mp "hyperpow_ge_zero";
 
 Goalw [hypreal_zero_def]
       "(0::hypreal) <= r --> 0 <= r pow n";
 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
 by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
-by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset,
-    realpow_ge_zero2],simpset() addsimps [hyperpow,hypreal_le]));
+by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset, realpow_ge_zero2],
+              simpset() addsimps [hyperpow,hypreal_le]));
 qed "hyperpow_ge_zero2";
 
 Goalw [hypreal_zero_def]
@@ -369,23 +367,23 @@
 
 Goalw [hypreal_one_def] "1hr pow n = 1hr";
 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [hyperpow]));
+by (auto_tac (claset(), simpset() addsimps [hyperpow]));
 qed "hyperpow_eq_one";
 Addsimps [hyperpow_eq_one];
 
 Goalw [hypreal_one_def]
       "abs(-(1hr pow n)) = 1hr";
 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [abs_one,
-    hrabs_minus_cancel,hyperpow,hypreal_hrabs]));
+by (auto_tac (claset(), 
+      simpset() addsimps [abs_one, hyperpow,hypreal_hrabs]));
 qed "hrabs_minus_hyperpow_one";
 Addsimps [hrabs_minus_hyperpow_one];
 
 Goalw [hypreal_one_def]
       "abs((-1hr) pow n) = 1hr";
 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps 
-    [hyperpow,hypreal_minus,hypreal_hrabs]));
+by (auto_tac (claset(),
+       simpset() addsimps [hyperpow,hypreal_minus,hypreal_hrabs]));
 qed "hrabs_hyperpow_minus_one";
 Addsimps [hrabs_hyperpow_minus_one];
 
@@ -393,8 +391,8 @@
 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
 by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
 by (res_inst_tac [("z","s")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hyperpow,
-    hypreal_mult,realpow_mult]));
+by (auto_tac (claset(),
+       simpset() addsimps [hyperpow, hypreal_mult,realpow_mult]));
 qed "hyperpow_mult";
 
 Goal "(0::hypreal) <= r pow (1hn + 1hn)";
@@ -413,13 +411,13 @@
 Addsimps [hyperpow_two_hrabs];
 
 Goal "!!r. 1hr < r ==> 1hr < r pow (1hn + 1hn)";
-by (auto_tac (claset(),simpset() addsimps [hyperpow_two]));
+by (auto_tac (claset(), simpset() addsimps [hyperpow_two]));
 by (cut_facts_tac [hypreal_zero_less_one] 1);
 by (forw_inst_tac [("R1.0","0")] hypreal_less_trans 1);
 by (assume_tac 1);
 by (dres_inst_tac [("z","r"),("x","1hr")] 
     hypreal_mult_less_mono1 1);
-by (auto_tac (claset() addIs [hypreal_less_trans],simpset()));
+by (auto_tac (claset() addIs [hypreal_less_trans], simpset()));
 qed "hyperpow_two_gt_one";
 
 Goal "!!r. 1hr <= r ==> 1hr <= r pow (1hn + 1hn)";
@@ -433,8 +431,8 @@
 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
 by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
 by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset]
-    addDs [realpow_Suc_gt_zero],simpset() addsimps [hyperpow,
-    hypreal_less,hypnat_add]));
+                       addDs [realpow_Suc_gt_zero], 
+              simpset() addsimps [hyperpow, hypreal_less,hypnat_add]));
 qed "hyperpow_Suc_gt_zero";
 
 Goal "!!r. (0::hypreal) <= r ==> 0 <= r pow (n + 1hn)";
@@ -456,8 +454,8 @@
 Goalw [hypreal_one_def]
       "(-1hr) pow ((1hn + 1hn)*n) = 1hr";
 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [hyperpow,
-    hypnat_add,hypreal_minus]));
+by (auto_tac (claset(),
+              simpset() addsimps [hyperpow, hypnat_add,hypreal_minus]));
 qed "hyperpow_minus_one2";
 Addsimps [hyperpow_minus_one2];
 
@@ -488,8 +486,8 @@
 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
 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 [hyperpow,
-    hypreal_le,hypreal_less,hypnat_less]));
+by (auto_tac (claset(),
+        simpset() addsimps [hyperpow, hypreal_le,hypreal_less,hypnat_less]));
 by (etac (FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset) 1);
 by (etac FreeUltrafilterNat_Int 1);
 by (auto_tac (claset() addSDs [conjI RS realpow_less_le],
@@ -510,12 +508,12 @@
 
 Goalw [hypreal_of_real_def,hypnat_of_nat_def] 
       "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)";
-by (auto_tac (claset(),simpset() addsimps [hyperpow]));
+by (auto_tac (claset(), simpset() addsimps [hyperpow]));
 qed "hyperpow_realpow";
 
 Goalw [SReal_def]
      "(hypreal_of_real r) pow (hypnat_of_nat n) : SReal";
-by (auto_tac (claset(),simpset() addsimps [hyperpow_realpow]));
+by (auto_tac (claset(), simpset() addsimps [hyperpow_realpow]));
 qed "hyperpow_SReal";
 Addsimps [hyperpow_SReal];
 
@@ -563,8 +561,7 @@
      "(x ^ n : Infinitesimal) = \
 \     (x pow (hypnat_of_nat n) : Infinitesimal)";
 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hrealpow,
-    hyperpow]));
+by (auto_tac (claset(), simpset() addsimps [hrealpow, hyperpow]));
 qed "hrealpow_hyperpow_Infinitesimal_iff";
 
 goal HyperPow.thy 
@@ -572,8 +569,8 @@
 \           ==> x ^ n : Infinitesimal";
 by (auto_tac (claset() addSIs [Infinitesimal_hyperpow],
     simpset() addsimps [hrealpow_hyperpow_Infinitesimal_iff,
-    hypnat_of_nat_less_iff,hypnat_of_nat_zero] 
-    delsimps [hypnat_of_nat_less_iff RS sym]));
+                        hypnat_of_nat_less_iff,hypnat_of_nat_zero] 
+              delsimps [hypnat_of_nat_less_iff RS sym]));
 qed "Infinitesimal_hrealpow";
 
 
diff -r 07f75bf77a33 -r c838477b5c18 src/HOL/Real/Hyperreal/Lim.ML
--- a/src/HOL/Real/Hyperreal/Lim.ML	Thu Dec 21 10:16:07 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Lim.ML	Thu Dec 21 10:16:33 2000 +0100
@@ -55,9 +55,8 @@
 qed "LIM_add";
 
 Goalw [LIM_def] "f -- a --> L ==> (%x. -f(x)) -- a --> -L";
-by (full_simp_tac (simpset() addsimps [real_minus_add_distrib RS sym,
-                                       abs_minus_cancel] 
-                    delsimps [real_minus_add_distrib,real_minus_minus]) 1);
+by (full_simp_tac (simpset() addsimps [real_minus_add_distrib RS sym] 
+                    delsimps [real_minus_add_distrib, real_minus_minus]) 1);
 qed "LIM_minus";
 
 (*----------------------------------------------
@@ -108,8 +107,7 @@
 Goal "[| f -- x --> L; f -- x --> M |] ==> L = M";
 by (dtac LIM_minus 1);
 by (dtac LIM_add 1 THEN assume_tac 1);
-by (auto_tac (claset() addSDs [LIM_const_eq RS sym],
-    simpset()));
+by (auto_tac (claset() addSDs [LIM_const_eq RS sym],  simpset()));
 qed "LIM_unique";
 
 (*-------------
@@ -142,7 +140,7 @@
 qed "LIM_mult_zero";
 
 Goalw [LIM_def] "(%x. x) -- a --> a";
-by (Auto_tac);
+by Auto_tac;
 qed "LIM_self";
 
 (*--------------------------------------------------------------
@@ -174,8 +172,7 @@
 by (Step_tac 1);
 by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1);
 by (auto_tac (claset(),
-      simpset() addsimps [real_add_minus_iff,
-                          starfun, hypreal_minus,hypreal_of_real_minus RS sym,
+      simpset() addsimps [real_add_minus_iff, starfun, hypreal_minus, 
                           hypreal_of_real_def, hypreal_add]));
 by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2 THEN Step_tac 1);
 by (dres_inst_tac [("x","u")] spec 1 THEN Clarify_tac 1);
@@ -230,15 +227,14 @@
 by (Step_tac 1);
 by (dres_inst_tac [("x","Abs_hypreal(hyprel^^{X})")] spec 1);
 by (asm_full_simp_tac
-    (simpset() addsimps [starfun,
-                         hypreal_minus,hypreal_of_real_minus RS sym,
+    (simpset() addsimps [starfun, hypreal_minus, 
                          hypreal_of_real_def,hypreal_add]) 1);
 by (Step_tac 1);
 by (dtac (lemma_simp RS real_seq_to_hypreal_Infinitesimal) 1);
 by (asm_full_simp_tac
     (simpset() addsimps 
        [Infinitesimal_FreeUltrafilterNat_iff,hypreal_of_real_def,
-        hypreal_minus,hypreal_of_real_minus,hypreal_add]) 1);
+        hypreal_minus, hypreal_add]) 1);
 by (Blast_tac 1); 
 by (rotate_tac 2 1);
 by (dres_inst_tac [("x","r")] spec 1);
@@ -264,14 +260,13 @@
 Goalw [NSLIM_def]
      "[| f -- x --NS> l; g -- x --NS> m |] \
 \     ==> (%x. f(x) * g(x)) -- x --NS> (l * m)";
-by (auto_tac (claset() addSIs [starfun_mult_HFinite_inf_close],
+by (auto_tac (claset() addSIs [inf_close_mult_HFinite],
               simpset() addsimps [hypreal_of_real_mult]));
 qed "NSLIM_mult";
 
 Goal "[| f -- x --> l; g -- x --> m |] \
 \     ==> (%x. f(x) * g(x)) -- x --> (l * m)";
-by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff,
-    NSLIM_mult]) 1);
+by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_mult]) 1);
 qed "LIM_mult2";
 
 (*----------------------------------------------
@@ -281,21 +276,20 @@
 Goalw [NSLIM_def]
      "[| f -- x --NS> l; g -- x --NS> m |] \
 \     ==> (%x. f(x) + g(x)) -- x --NS> (l + m)";
-by (auto_tac (claset() addSIs [starfun_add_inf_close],
+by (auto_tac (claset() addSIs [inf_close_add],
               simpset() addsimps [hypreal_of_real_add]));
 qed "NSLIM_add";
 
 Goal "[| f -- x --> l; g -- x --> m |] \
 \     ==> (%x. f(x) + g(x)) -- x --> (l + m)";
-by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff,
-    NSLIM_add]) 1);
+by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_add]) 1);
 qed "LIM_add2";
 
 (*----------------------------------------------
      NSLIM_const
  ----------------------------------------------*)
 Goalw [NSLIM_def] "(%x. k) -- x --NS> k";
-by (Auto_tac);
+by Auto_tac;
 qed "NSLIM_const";
 
 Addsimps [NSLIM_const];
@@ -309,14 +303,11 @@
  ----------------------------------------------*)
 Goalw [NSLIM_def] 
       "f -- a --NS> L ==> (%x. -f(x)) -- a --NS> -L";
-by (auto_tac (claset() addIs [inf_close_minus],
-    simpset() addsimps [starfun_minus RS sym,
-    hypreal_of_real_minus]));
+by Auto_tac;  
 qed "NSLIM_minus";
 
 Goal "f -- a --> L ==> (%x. -f(x)) -- a --> -L";
-by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff,
-    NSLIM_minus]) 1);
+by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_minus]) 1);
 qed "LIM_minus2";
 
 (*----------------------------------------------
@@ -346,7 +337,6 @@
                                   hypreal_of_real_inverse RS sym]));
 by (forward_tac [inf_close_hypreal_of_real_not_zero] 1 THEN assume_tac 1);
 by (dtac hypreal_of_real_HFinite_diff_Infinitesimal 1);
-by (stac (starfun_inverse RS sym) 1);
 by (auto_tac (claset() addSEs [inf_close_inverse],
               simpset() addsimps [hypreal_of_real_zero_iff]));
 qed "NSLIM_inverse";
@@ -387,7 +377,7 @@
    NSLIM_not_zero
  --------------------------*)
 Goalw [NSLIM_def] "k ~= #0 ==> ~ ((%x. k) -- x --NS> #0)";
-by (Auto_tac);
+by Auto_tac;
 by (res_inst_tac [("x","hypreal_of_real x + ehr")] exI 1);
 by (auto_tac (claset() addIs [Infinitesimal_add_inf_close_self 
     RS inf_close_sym],simpset()));
@@ -482,10 +472,10 @@
 
 Goalw [isNSCont_def,NSLIM_def] 
       "f -- a --NS> (f a) ==> isNSCont f a";
-by (Auto_tac);
+by Auto_tac;
 by (res_inst_tac [("Q","y = hypreal_of_real a")] 
     (excluded_middle RS disjE) 1);
-by (Auto_tac);
+by Auto_tac;
 qed "NSLIM_isNSCont";
 
 (*-----------------------------------------------------
@@ -569,16 +559,18 @@
      sum continuous
  ------------------------*)
 Goal "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) + g(x)) a";
-by (auto_tac (claset() addIs [starfun_add_inf_close],simpset() addsimps 
-              [isNSCont_isCont_iff RS sym,isNSCont_def,hypreal_of_real_add]));
+by (auto_tac (claset() addIs [inf_close_add],
+              simpset() addsimps [isNSCont_isCont_iff RS sym, isNSCont_def,
+                             hypreal_of_real_add]));
 qed "isCont_add";
 
 (*------------------------
      mult continuous
  ------------------------*)
 Goal "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) * g(x)) a";
-by (auto_tac (claset() addSIs [starfun_mult_HFinite_inf_close],simpset() addsimps 
-              [isNSCont_isCont_iff RS sym,isNSCont_def,hypreal_of_real_mult]));
+by (auto_tac (claset() addSIs [starfun_mult_HFinite_inf_close],
+              simpset() delsimps [starfun_mult RS sym]
+			addsimps [isNSCont_isCont_iff RS sym, isNSCont_def, hypreal_of_real_mult]));
 qed "isCont_mult";
 
 (*-------------------------------------------
@@ -597,8 +589,7 @@
 qed "isCont_o2";
 
 Goalw [isNSCont_def] "isNSCont f a ==> isNSCont (%x. - f x) a";
-by (auto_tac (claset(),simpset() addsimps [starfun_minus RS sym, 
-    hypreal_of_real_minus])); 
+by Auto_tac; 
 qed "isNSCont_minus";
 
 Goal "isCont f a ==> isCont (%x. - f x) a";
@@ -632,13 +623,14 @@
 Addsimps [isNSCont_const];
 
 Goalw [isNSCont_def]  "isNSCont abs a";
-by (auto_tac (claset() addIs [inf_close_hrabs],simpset() addsimps 
-    [hypreal_of_real_hrabs RS sym,starfun_rabs_hrabs]));
+by (auto_tac (claset() addIs [inf_close_hrabs],
+              simpset() addsimps [hypreal_of_real_hrabs RS sym,
+                                  starfun_rabs_hrabs]));
 qed "isNSCont_rabs";
 Addsimps [isNSCont_rabs];
 
 Goal "isCont abs a";
-by (auto_tac (claset(),simpset() addsimps [isNSCont_isCont_iff RS sym]));
+by (auto_tac (claset(), simpset() addsimps [isNSCont_isCont_iff RS sym]));
 qed "isCont_rabs";
 Addsimps [isCont_rabs];
 
@@ -756,7 +748,7 @@
 \         {n. abs (X n + - Y n) < inverse (real_of_posnat  n) & \
 \             r <= abs (f (X n) + - f(Y n))} <= \
 \         {n. r <= abs (Ya n)}";
-by (Auto_tac);
+by Auto_tac;
 val lemma_Intu = result ();
 
 Goalw [isNSUCont_def,isUCont_def,inf_close_def] 
@@ -771,7 +763,7 @@
 by (dres_inst_tac [("x","Abs_hypreal(hyprel^^{Y})")] spec 1);
 by (asm_full_simp_tac (simpset() addsimps [starfun,
     hypreal_minus,hypreal_add]) 1);
-by (Auto_tac);
+by Auto_tac;
 by (dtac (lemma_simpu RS real_seq_to_hypreal_Infinitesimal2) 1);
 by (asm_full_simp_tac (simpset() addsimps 
     [Infinitesimal_FreeUltrafilterNat_iff,
@@ -884,9 +876,7 @@
 by (rtac ccontr 3);
 by (dres_inst_tac [("x","h")] spec 3);
 by (auto_tac (claset(),
-              simpset() addsimps [mem_infmal_iff,
-            starfun_divide RS sym, starfun_add RS sym,
-            hypreal_of_real_minus, starfun_lambda_cancel]));
+              simpset() addsimps [mem_infmal_iff, starfun_lambda_cancel]));
 qed "NSDERIV_NSLIM_iff";
 
 (*--- second equivalence ---*)
@@ -947,9 +937,7 @@
 by (subgoal_tac "(*f* (%z. z - x)) xa ~= (0::hypreal)" 2);
 by (rotate_tac ~1 2);
 by (auto_tac (claset(),
-    simpset() addsimps [starfun_divide RS sym, 
-			starfun_add RS sym, real_diff_def, 
-			hypreal_of_real_minus, hypreal_diff_def, 
+    simpset() addsimps [real_diff_def, hypreal_diff_def, 
 		(inf_close_minus_iff RS iffD1) RS (mem_infmal_iff RS iffD2),  
 			Infinitesimal_subset_HFinite RS subsetD]));
 qed "NSDERIVD5";
@@ -1048,9 +1036,9 @@
 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff,
            NSLIM_def]) 1 THEN REPEAT(Step_tac 1));
 by (auto_tac (claset(),
-       simpset() addsimps [starfun_divide RS sym, starfun_add RS sym,
-    hypreal_of_real_minus, hypreal_of_real_add, hypreal_of_real_divide,
-    hypreal_add_divide_distrib]));
+       simpset() addsimps [hypreal_of_real_add, 
+                           hypreal_of_real_divide,
+                           hypreal_add_divide_distrib]));
 by (thin_tac "xa @= hypreal_of_real #0" 1 THEN dtac inf_close_add 1);
 by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
 qed "NSDERIV_add";
@@ -1068,10 +1056,10 @@
  ----------------------------------------------------*)
 (* lemma - terms manipulation tedious as usual*)
 
-Goal "((a::real)*b) + -(c*d) = (b*(a + -c)) + \
+Goal "((a::hypreal)*b) + -(c*d) = (b*(a + -c)) + \
 \                           (c*(b + -d))";
-by (full_simp_tac (simpset() addsimps [real_add_mult_distrib2,
-    real_minus_mult_eq2 RS sym,real_mult_commute]) 1);
+by (full_simp_tac (simpset() addsimps [hypreal_add_mult_distrib2,
+    hypreal_minus_mult_eq2 RS sym,hypreal_mult_commute]) 1);
 val lemma_nsderiv1 = result();
 
 Goal "[| (x + y) / z = hypreal_of_real D + yb; z ~= 0; \
@@ -1085,20 +1073,19 @@
 by (etac (Infinitesimal_subset_HFinite RS subsetD) 1);
 val lemma_nsderiv2 = result();
 
+
 Goal "[| NSDERIV f x :> Da; NSDERIV g x :> Db |] \
 \     ==> NSDERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))";
 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff, NSLIM_def]) 1 
     THEN REPEAT(Step_tac 1));
 by (auto_tac (claset(),
-       simpset() addsimps [starfun_divide RS sym, starfun_mult RS sym,
-              starfun_add RS sym,starfun_lambda_cancel,hypreal_of_real_zero,
+       simpset() addsimps [starfun_lambda_cancel, hypreal_of_real_zero,
               lemma_nsderiv1]));
-by (simp_tac (simpset() addsimps [hypreal_add_divide_distrib]) 1);
+by (simp_tac (simpset() addsimps [hypreal_add_divide_distrib]) 1); 
 by (REPEAT(dtac (bex_Infinitesimal_iff2 RS iffD2) 1));
 by (auto_tac (claset(),
         simpset() delsimps [hypreal_times_divide1_eq]
-		  addsimps [hypreal_times_divide1_eq RS sym, 
-                            hypreal_of_real_minus]));
+		  addsimps [hypreal_times_divide1_eq RS sym]));
 by (dres_inst_tac [("D","Db")] lemma_nsderiv2 1);
 by (dtac (inf_close_minus_iff RS iffD2 RS (bex_Infinitesimal_iff2 RS iffD2)) 4);
 by (auto_tac (claset() addSIs [inf_close_add_mono1],
@@ -1148,13 +1135,12 @@
 (*--------------------------------
    Negation of function
  -------------------------------*)
-Goal "NSDERIV f x :> D \
-\      ==> NSDERIV (%x. -(f x)) x :> -D";
+Goal "NSDERIV f x :> D ==> NSDERIV (%x. -(f x)) x :> -D";
 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff]) 1);
 by (res_inst_tac [("t","f x")] (real_minus_minus RS subst) 1);
 by (asm_simp_tac (simpset() addsimps [real_minus_add_distrib RS sym,
-    real_minus_mult_eq1 RS sym] delsimps [real_minus_add_distrib,
-    real_minus_minus]) 1);
+                                      real_minus_mult_eq1 RS sym] 
+                   delsimps [real_minus_add_distrib, real_minus_minus]) 1);
 by (etac NSLIM_minus 1);
 qed "NSDERIV_minus";
 
@@ -1254,7 +1240,7 @@
 \              xa ~= 0 \
 \           |] ==> D = #0";
 by (dtac bspec 1);
-by (Auto_tac);
+by Auto_tac;
 by (asm_full_simp_tac (simpset() addsimps [hypreal_of_real_zero RS sym]) 1);
 qed "NSDERIV_zero";
 
@@ -1267,7 +1253,7 @@
     [mem_infmal_iff RS sym]) 1);
 by (rtac Infinitesimal_ratio 1);
 by (rtac inf_close_hypreal_of_real_HFinite 3);
-by (Auto_tac);
+by Auto_tac;
 qed "NSDERIV_inf_close";
 
 (*--------------------------------------------------------------- 
@@ -1285,9 +1271,7 @@
 \             / ((*f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real (g x)) \
 \            @= hypreal_of_real(Da)";
 by (auto_tac (claset(),
-       simpset() addsimps [NSDERIV_NSLIM_iff2, NSLIM_def, starfun_divide RS sym,
-                           hypreal_of_real_minus,
-                           starfun_add RS sym]));
+       simpset() addsimps [NSDERIV_NSLIM_iff2, NSLIM_def]));
 qed "NSDERIVD1";
 
 (*-------------------------------------------------------------- 
@@ -1301,9 +1285,8 @@
 \     ==> ((*f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real(g x)) / xa \
 \         @= hypreal_of_real(Db)";
 by (auto_tac (claset(),
-    simpset() addsimps [NSDERIV_NSLIM_iff, NSLIM_def, starfun_divide RS sym,
-		starfun_add RS sym, hypreal_of_real_zero, mem_infmal_iff,
-		starfun_lambda_cancel,hypreal_of_real_minus]));
+    simpset() addsimps [NSDERIV_NSLIM_iff, NSLIM_def, 
+		hypreal_of_real_zero, mem_infmal_iff, starfun_lambda_cancel]));
 qed "NSDERIVD2";
 
 (*---------------------------------------------
@@ -1315,9 +1298,9 @@
 by (asm_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff,
     NSLIM_def,hypreal_of_real_zero,mem_infmal_iff RS sym]) 1 THEN Step_tac 1);
 by (forw_inst_tac [("f","g")] NSDERIV_inf_close 1);
-by (auto_tac (claset(),simpset() addsimps [starfun_add RS sym,
-    hypreal_of_real_minus, hypreal_of_real_mult,
-    starfun_lambda_cancel2,starfun_o RS sym, starfun_divide RS sym]));
+by (auto_tac (claset(),
+    simpset() addsimps [hypreal_of_real_mult,
+              starfun_lambda_cancel2, starfun_o RS sym]));
 by (case_tac "(*f* g) (hypreal_of_real(x) + xa) = hypreal_of_real (g x)" 1);
 by (dres_inst_tac [("g","g")] NSDERIV_zero 1);
 by (auto_tac (claset(),
@@ -1351,7 +1334,7 @@
 Goal "NSDERIV (%x. x) x :> #1";
 by (auto_tac (claset(),
      simpset() addsimps [NSDERIV_NSLIM_iff,
-          NSLIM_def, starfun_divide RS sym,starfun_Id, hypreal_of_real_zero,
+          NSLIM_def ,starfun_Id, hypreal_of_real_zero,
            hypreal_of_real_one]));
 qed "NSDERIV_Id";
 Addsimps [NSDERIV_Id];
@@ -1396,31 +1379,15 @@
                     Power of -1 
  ---------------------------------------------------------------*)
 
-
-
-(*??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))";
 by (rtac ballI 1 THEN Asm_full_simp_tac 1 THEN Step_tac 1);
 by (forward_tac [Infinitesimal_add_not_zero] 1);
+by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 2); 
 by (auto_tac (claset(),
      simpset() addsimps [starfun_inverse_inverse,
-         hypreal_of_real_inverse RS sym,hypreal_of_real_minus,realpow_two,
+         hypreal_of_real_inverse RS sym, realpow_two,
          hypreal_of_real_mult,
          hypreal_of_real_divide] 
                delsimps [hypreal_minus_mult_eq1 RS sym,
@@ -1432,16 +1399,6 @@
           @ 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, 
@@ -1449,8 +1406,10 @@
 by (dres_inst_tac [("x3","x") ] ((HFinite_hypreal_of_real RSN
          (2,Infinitesimal_HFinite_mult2)) RS  
           (Infinitesimal_minus_iff RS iffD1)) 1); 
-by (forw_inst_tac [("x","hypreal_of_real x"),("y","hypreal_of_real x")] hypreal_mult_not_0 1);
-by (res_inst_tac [("y"," inverse(- hypreal_of_real x * hypreal_of_real x)")] inf_close_trans 2);
+by (forw_inst_tac [("x","hypreal_of_real x"),("y","hypreal_of_real x")]
+       hypreal_mult_not_0 1);
+by (res_inst_tac [("y"," inverse(- hypreal_of_real x * hypreal_of_real x)")] 
+                 inf_close_trans 2);
 by (rtac inverse_add_Infinitesimal_inf_close2 2);
 by (auto_tac (claset() addIs [HFinite_minus_iff RS iffD1]
          addSDs [Infinitesimal_minus_iff RS iffD2,
@@ -1533,11 +1492,9 @@
 \     ==> NSDERIV f x :> l";
 by (auto_tac (claset(), 
               simpset() delsimprocs real_cancel_factor
-                        addsimps [NSDERIV_iff2, starfun_mult RS sym, 
-                                  starfun_divide RS sym]));
+                        addsimps [NSDERIV_iff2]));
 by (auto_tac (claset(),
-              simpset() addsimps [hypreal_mult_assoc,
-                                  starfun_diff RS sym]));
+              simpset() addsimps [hypreal_mult_assoc]));
 by (asm_full_simp_tac (simpset() addsimps [hypreal_eq_minus_iff3 RS sym,
                                            hypreal_diff_def]) 1);
 by (asm_full_simp_tac (simpset() addsimps [isNSCont_def]) 1);
@@ -1545,16 +1502,16 @@
  
 
 
-(*----------------------------------------------------------------------------*)
-(* Useful lemmas about nested intervals and proof by bisection (cf.Harrison)  *)
-(*----------------------------------------------------------------------------*)
+(*--------------------------------------------------------------------------*)
+(* Lemmas about nested intervals and proof by bisection (cf.Harrison)       *)
+(* All considerably tidied by lcp                                           *)
+(*--------------------------------------------------------------------------*)
 
 Goal "(ALL n. (f::nat=>real) n <= f (Suc n)) --> f m <= f(m + no)";
 by (induct_tac "no" 1);
 by (auto_tac (claset() addIs [real_le_trans],simpset()));
 qed_spec_mp "lemma_f_mono_add";
 
-
 Goal "[| ALL n. f(n) <= f(Suc n); \
 \        ALL n. g(Suc n) <= g(n); \
 \        ALL n. f(n) <= g(n) |] \
@@ -1588,7 +1545,7 @@
 by (subgoal_tac "lim f <= f(no + n)" 1);
 by (induct_tac "no" 2);
 by (auto_tac (claset() addIs [real_le_trans],
-              simpset() addsimps [real_diff_def, abs_real_def]));
+              simpset() addsimps [real_diff_def, real_abs_def]));
 by (dres_inst_tac [("i","f(no + n)"),("no1","no")] 
     (lemma_f_mono_add RSN (2,real_less_le_trans)) 1);
 by (auto_tac (claset(), simpset() addsimps [add_commute]));
@@ -1625,7 +1582,6 @@
                                   convergent_LIMSEQ_iff]));  
 qed "lemma_nest";
 
-
 Goal "[| ALL n. f(n) <= f(Suc n); \
 \        ALL n. g(Suc n) <= g(n); \
 \        ALL n. f(n) <= g(n); \
@@ -1638,15 +1594,29 @@
 by (auto_tac (claset() addIs [LIMSEQ_unique], simpset()));
 qed "lemma_nest_unique";
 
-Goal "EX! fn. (fn 0 = e) & (ALL n. fn (Suc n) = f n (fn n))";
-by (rtac ex1I 1);
-by (rtac conjI 1 THEN rtac allI 2);
-by (rtac def_nat_rec_0 1 THEN rtac def_nat_rec_Suc 2);
-by (Auto_tac);
-by (rtac ext 1 THEN induct_tac "n" 1);
-by (Auto_tac);
-qed "nat_Axiom";
+
+Goal "a <= b ==> \
+\  ALL n. fst (Bolzano_bisect P a b n) <= snd (Bolzano_bisect P a b n)";
+by (rtac allI 1);
+by (induct_tac "n" 1);
+by (auto_tac (claset(), simpset() addsimps [Let_def, split_def]));  
+qed "Bolzano_bisect_le";
 
+Goal "a <= b ==> \
+\  ALL n. fst(Bolzano_bisect P a b n) <= fst (Bolzano_bisect P a b (Suc n))";
+by (rtac allI 1);
+by (induct_tac "n" 1);
+by (auto_tac (claset(), 
+              simpset() addsimps [Bolzano_bisect_le, Let_def, split_def]));  
+qed "Bolzano_bisect_fst_le_Suc";
+
+Goal "a <= b ==> \
+\  ALL n. snd(Bolzano_bisect P a b (Suc n)) <= snd (Bolzano_bisect P a b n)";
+by (rtac allI 1);
+by (induct_tac "n" 1);
+by (auto_tac (claset(), 
+              simpset() addsimps [Bolzano_bisect_le, Let_def, split_def]));  
+qed "Bolzano_bisect_Suc_le_snd";
 
 Goal "((x::real) = y / (#2 * z)) = (#2 * x = y/z)";
 by Auto_tac;  
@@ -1654,131 +1624,90 @@
 by Auto_tac;  
 qed "eq_divide_2_times_iff";
 
+Goal "a <= b ==> \
+\     snd(Bolzano_bisect P a b n) - fst(Bolzano_bisect P a b n) = \
+\     (b-a) / (#2 ^ n)";
+by (induct_tac "n" 1);
+by (auto_tac (claset(), 
+      simpset() addsimps [eq_divide_2_times_iff, real_add_divide_distrib, 
+                          Let_def, split_def]));
+by (auto_tac (claset(), 
+              simpset() addsimps [Bolzano_bisect_le, real_diff_def]));  
+qed "Bolzano_bisect_diff";
 
-val [prem1,prem2] =
-Goal "[| !!a b c. [| a <= b; b <= c; P(a,b); P(b,c)|] ==> P(a,c); \
+val Bolzano_nest_unique =
+    [Bolzano_bisect_fst_le_Suc, Bolzano_bisect_Suc_le_snd, Bolzano_bisect_le] 
+    MRS lemma_nest_unique;
+
+(*P_prem is a looping simprule, so it works better if it isn't an assumption*)
+val P_prem::notP_prem::rest =
+Goal "[| !!a b c. [| P(a,b); P(b,c); a <= b; b <= c|] ==> P(a,c); \
+\        ~ P(a,b);  a <= b |] ==> \
+\     ~ P(fst(Bolzano_bisect P a b n), snd(Bolzano_bisect P a b n))";
+by (cut_facts_tac rest 1);
+by (induct_tac "n" 1);
+by (auto_tac (claset(), 
+              simpset() delsimps [surjective_pairing RS sym]
+			addsimps [notP_prem, Let_def, split_def]));  
+by (swap_res_tac [P_prem] 1);
+by (assume_tac 1); 
+by (auto_tac (claset(), simpset() addsimps [Bolzano_bisect_le]));  
+qed "not_P_Bolzano_bisect";
+
+(*Now we re-package P_prem as a formula*)
+Goal "[| ALL a b c. P(a,b) & P(b,c) & a <= b & b <= c --> P(a,c); \
+\        ~ P(a,b);  a <= b |] ==> \
+\     ALL n. ~ P(fst(Bolzano_bisect P a b n), snd(Bolzano_bisect P a b n))";
+by (blast_tac (claset() addSEs [not_P_Bolzano_bisect RSN (2,rev_notE)]) 1); 
+qed "not_P_Bolzano_bisect'";
+
+
+Goal "[| ALL a b c. P(a,b) & P(b,c) & a <= b & b <= c --> P(a,c); \
 \        ALL x. EX d::real. 0 < d & \
-\               (ALL a b. a <= x & x <= b & (b - a) < d --> P(a,b)) \
-\     |] ==> ALL a b. a <= b --> P(a,b)";
-by (Step_tac 1);
-by (cut_inst_tac [("e","(a,b)"),
-    ("f","%n fn. if P(fst fn, (fst fn + snd fn)/#2) \
-\              then ((fst fn + snd fn) /#2,snd fn) \
-\              else (fst fn,(fst fn + snd fn)/#2)")] 
-    nat_Axiom 1);
-by (etac ex1E 1 THEN etac conjE 1 THEN rtac ccontr 1);
-(* set up 1st premise of lemma_nest_unique *)
-by (subgoal_tac "ALL n. fst((fn::nat =>(real*real)) n) <= snd (fn n)" 1);
-by (rtac allI 2);
-by (induct_tac "n" 2);
-by (Asm_simp_tac 2);
-by (dres_inst_tac [("x","na")] spec 2);
-by (case_tac "P (fst (fn na), (fst (fn na) + snd (fn na)) / #2)" 2);
-by (Asm_simp_tac 3);
-by (Asm_simp_tac 2);
-(* 2nd premise *) 
-by (subgoal_tac "ALL n. fst(fn n) <= fst (fn (Suc n))" 1);
-by (rtac allI 2);
-by (induct_tac "n" 2);
-by (dres_inst_tac [("x","0")] spec 2);
-by (Asm_simp_tac 3);  (*super slow, but proved!*)
-by (Asm_simp_tac 2);
-(* 3rd premise? [lcp] *)
-by (subgoal_tac "ALL n. ~P(fst(fn n),snd(fn n))" 1);
-by (rtac allI 2);
-by (induct_tac "n" 2);
-by (Asm_simp_tac 2);
-by (Asm_simp_tac 2 THEN rtac impI 2);
-by (rtac ccontr 2);
-by (res_inst_tac [("Pa","P (fst (fn na), snd (fn na))")] swap 2);
-by (assume_tac 2);
-by (res_inst_tac [("b","(fst(fn na) + snd(fn na))/#2")] prem1 2);
-by (Asm_full_simp_tac 4); 
-by (Asm_full_simp_tac 4); 
-by (Asm_full_simp_tac 2); 
-by (Asm_simp_tac 2); 
-(* 3rd premise [looks like the 4th to lcp!] *)
-by (subgoal_tac "ALL n. snd(fn (Suc n)) <= snd (fn n)" 1);
-by (rtac allI 2);
-by (induct_tac "n" 2);
-by (Asm_simp_tac 2);
-by (Asm_simp_tac 2);
-(* FIXME: simplification takes a very long time! *)
-by (ALLGOALS(thin_tac "ALL y. \
-\            y 0 = (a, b) & \
-\            (ALL n. \
-\                y (Suc n) = \
-\                (if P (fst (y n), (fst (y n) + snd (y n)) /#2) \
-\                 then ((fst (y n) + snd (y n)) /#2, snd (y n)) \
-\                 else (fst (y n),\
-\                       (fst (y n) + snd (y n)) /#2))) --> \
-\            y = fn"));
-(*another premise? the 5th? lcp*)
-by (subgoal_tac "ALL n. snd(fn n) - fst(fn n) = \
-\                       (b - a) * inverse(#2 ^ n)" 1);
-by (rtac allI 2);
-by (induct_tac "n" 2);
-by (Asm_simp_tac 2);
-by (asm_full_simp_tac
-    (simpset() addsimps [eq_divide_2_times_iff, real_inverse_eq_divide,
-                         real_diff_mult_distrib2]) 2);
-(*end of the premises [lcp]*)
-by (dtac lemma_nest_unique 1);
-by (REPEAT(assume_tac 1));
-by (Step_tac 2);
+\               (ALL a b. a <= x & x <= b & (b - a) < d --> P(a,b)); \
+\        a <= b |]  \
+\     ==> P(a,b)";
+by (rtac (inst "P1" "P" Bolzano_nest_unique RS exE) 1);
+by (REPEAT (assume_tac 1));
 by (rtac LIMSEQ_minus_cancel 1);
-by (asm_simp_tac (simpset() addsimps [CLAIM "-((a::real) - b) = (b - a)",
-    realpow_inverse]) 1);
-by (subgoal_tac "#0 = (b-a) * #0" 1);
-by (eres_inst_tac [("t","#0")] ssubst 1); 
-by (rtac (LIMSEQ_const RS LIMSEQ_mult) 1);
-by (rtac LIMSEQ_realpow_zero 1);
-by (Asm_full_simp_tac 3); 
-by (EVERY1[Simp_tac, Simp_tac]);
-by (cut_facts_tac [prem2] 1);
-by (dres_inst_tac [("x","l")] spec 1 THEN Step_tac 1);
+by (asm_simp_tac (simpset() addsimps [Bolzano_bisect_diff,
+                                      LIMSEQ_divide_realpow_zero]) 1); 
+by (rtac ccontr 1);
+by (dtac not_P_Bolzano_bisect' 1); 
+by (REPEAT (assume_tac 1));
+by (rename_tac "l" 1);
+by (dres_inst_tac [("x","l")] spec 1 THEN Clarify_tac 1);
 by (rewtac LIMSEQ_def);
-by (dres_inst_tac [("x","d/#2")] spec 1);
-by (dres_inst_tac [("x","d/#2")] spec 1);
+by (dres_inst_tac [("P", "%r. #0<r --> ?Q r"), ("x","d/#2")] spec 1);
+by (dres_inst_tac [("P", "%r. #0<r --> ?Q r"), ("x","d/#2")] spec 1);
 by (dtac real_less_half_sum 1);
-by (thin_tac "ALL n. \
-\             fn (Suc n) = \
-\             (if P (fst (fn n), (fst (fn n) + snd (fn n))/#2) \
-\              then ((fst (fn n) + snd (fn n))/#2, snd (fn n)) \
-\              else (fst (fn n), \
-\                    (fst (fn n) + snd (fn n))/#2))" 1);
-by (Step_tac 1);
-by (ALLGOALS(Asm_full_simp_tac));
-by (dres_inst_tac [("x","fst(fn (no + noa))")] spec 1);
-by (dres_inst_tac [("x","snd(fn (no + noa))")] spec 1);
-by (Step_tac 1);
-by (ALLGOALS(Asm_full_simp_tac));
-by (res_inst_tac [("j","abs(fst(fn(no + noa)) - l) + \
-\                       abs(snd(fn(no + noa)) - l)")] real_le_less_trans 1);
-by (rtac (real_sum_of_halves RS subst) 2);
-by (rewtac real_diff_def);
-by (rtac real_add_less_mono 2);
-
-by (Asm_full_simp_tac 2); 
-by (Asm_full_simp_tac 2); 
-by (res_inst_tac [("y1","fst(fn (no + noa)) ")] 
-    (abs_minus_add_cancel RS subst) 1);
-by (subgoal_tac "#0 <= (l + - fst (fn (no + noa)))" 1);
-by (subgoal_tac "#0 <= (snd (fn (no + noa)) + - l)" 1);
-by (asm_simp_tac (simpset() addsimps [abs_eqI1] @ real_add_ac) 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps real_add_divide_distrib::real_add_ac)));
+by Safe_tac;
+(*linear arithmetic bug if we just use Asm_simp_tac*)
+by (ALLGOALS Asm_full_simp_tac);
+by (dres_inst_tac [("x","fst(Bolzano_bisect P a b (no + noa))")] spec 1);
+by (dres_inst_tac [("x","snd(Bolzano_bisect P a b (no + noa))")] spec 1);
+by Safe_tac;
+by (ALLGOALS Asm_simp_tac);
+by (res_inst_tac [("j","abs(fst(Bolzano_bisect P a b(no + noa)) - l) + \
+\                       abs(snd(Bolzano_bisect P a b(no + noa)) - l)")] 
+    real_le_less_trans 1);
+by (asm_simp_tac (simpset() addsimps [real_abs_def]) 1);  
+by (rtac (real_sum_of_halves RS subst) 1);
+by (rtac real_add_less_mono 1);
+by (ALLGOALS 
+    (asm_full_simp_tac (simpset() addsimps [symmetric real_diff_def])));
 qed "lemma_BOLZANO";
 
+
 Goal "((ALL a b c. (a <= b & b <= c & P(a,b) & P(b,c)) --> P(a,c)) & \
-\         (ALL x. EX d::real. 0 < d & \
+\      (ALL x. EX d::real. 0 < d & \
 \               (ALL a b. a <= x & x <= b & (b - a) < d --> P(a,b)))) \
-\         --> (ALL a b. a <= b --> P(a,b))";
-by (Step_tac 1);
-by (rtac (lemma_BOLZANO RS allE) 1);
-by (assume_tac 2);
-by (ALLGOALS(Blast_tac));
+\     --> (ALL a b. a <= b --> P(a,b))";
+by (Clarify_tac 1);
+by (blast_tac (claset() addIs [lemma_BOLZANO]) 1); 
 qed "lemma_BOLZANO2";
 
+
 (*----------------------------------------------------------------------------*)
 (* Intermediate Value Theorem (prove contrapositive by bisection)             *)
 (*----------------------------------------------------------------------------*)
@@ -1906,7 +1835,7 @@
 by (auto_tac (claset() addIs [abs_triangle_ineq RSN (2, real_le_trans)],
               simpset() addsimps [real_diff_def,abs_ge_self]));
 by (auto_tac (claset(),
-              simpset() addsimps [abs_real_def] addsplits [split_if_asm]));
+              simpset() addsimps [real_abs_def] addsplits [split_if_asm]));
 qed "isCont_bounded";
 
 (*----------------------------------------------------------------------------*)
@@ -1923,7 +1852,7 @@
 \                  (ALL N. N < M --> (EX x. a <= x & x <= b & N < f(x)))";
 by (cut_inst_tac [("S","Collect (%y. EX x. a <= x & x <= b & y = f x)")]
     lemma_reals_complete 1);
-by (Auto_tac);
+by Auto_tac;
 by (dtac isCont_bounded 1 THEN assume_tac 1);
 by (auto_tac (claset(),simpset() addsimps [isUb_def,leastP_def,
     isLub_def,setge_def,setle_def]));
@@ -2000,7 +1929,7 @@
 by (blast_tac (claset() addIs [isCont_minus]) 2);
 by (dres_inst_tac [("f","(%x. -(f x))")] isCont_eq_Ub 1);
 by (Step_tac 1);
-by (Auto_tac);
+by Auto_tac;
 qed "isCont_eq_Lb";
 
 
@@ -2042,7 +1971,7 @@
 by (asm_full_simp_tac (simpset() addsimps [real_0_less_mult_iff]) 2); 
 by (dres_inst_tac [("x","h")] spec 1);
 by (asm_full_simp_tac
-    (simpset() addsimps [abs_real_def, real_inverse_eq_divide, 
+    (simpset() addsimps [real_abs_def, real_inverse_eq_divide, 
                  pos_real_le_divide_eq, pos_real_less_divide_eq]
               addsplits [split_if_asm]) 1); 
 qed "DERIV_left_inc";
@@ -2056,7 +1985,7 @@
 by (asm_full_simp_tac (simpset() addsimps [real_mult_less_0_iff]) 2); 
 by (dres_inst_tac [("x","-h")] spec 1);
 by (asm_full_simp_tac
-    (simpset() addsimps [abs_real_def, real_inverse_eq_divide, 
+    (simpset() addsimps [real_abs_def, real_inverse_eq_divide, 
                          pos_real_less_divide_eq,
                          symmetric real_diff_def]
                addsplits [split_if_asm]) 1);
@@ -2080,7 +2009,7 @@
 by (Step_tac 1);
 by (dres_inst_tac [("x","x - e")] spec 1);
 by (dres_inst_tac [("x","x + e")] spec 2);
-by (auto_tac (claset(),simpset() addsimps [abs_eqI2,abs_minus_cancel]));
+by (auto_tac (claset(), simpset() addsimps [abs_eqI2]));
 qed "DERIV_local_max";
 
 (*----------------------------------------------------------------------------*)
@@ -2116,14 +2045,14 @@
 by (Step_tac 1);
 by (res_inst_tac [("x","x - a")] exI 1);
 by (res_inst_tac [("x","b - x")] exI 2);
-by (Auto_tac);
+by Auto_tac;
 by (auto_tac (claset(),simpset() addsimps [real_less_diff_eq]));
 qed "lemma_interval_lt";
 
 Goal "[| a < x;  x < b |] ==> \
 \       EX d::real. #0 < d &  (ALL y. abs(x - y) < d --> a <= y & y <= b)";
 by (dtac lemma_interval_lt 1);
-by (Auto_tac);
+by Auto_tac;
 by (auto_tac (claset() addSIs [exI] ,simpset()));
 qed "lemma_interval";
 
@@ -2270,7 +2199,7 @@
 by (dres_inst_tac [("x","a")] real_le_imp_less_or_eq 1);
 by (Step_tac 1);
 by (dres_inst_tac [("b","x")] DERIV_isconst_end 1);
-by (Auto_tac);
+by Auto_tac;
 qed "DERIV_isconst1";
 
 Goal "[| a < b; \
@@ -2289,7 +2218,7 @@
 
 Goal "[|a ~= b; ALL x. DERIV f x :> k |] ==> (f(b) - f(a)) = (b - a) * k";
 by (res_inst_tac [("R1.0","a"),("R2.0","b")] real_linear_less2 1);
-by (Auto_tac);
+by Auto_tac;
 by (ALLGOALS(dres_inst_tac [("f","f")] MVT));
 by (auto_tac (claset() addDs [DERIV_isCont,DERIV_unique],simpset() addsimps 
     [differentiable_def]));
@@ -2319,7 +2248,7 @@
 Goal "[|a ~= (b::real); ALL x. DERIV v x :> k|] \
 \     ==> v((a + b)/#2) = (v a + v b)/#2";
 by (res_inst_tac [("R1.0","a"),("R2.0","b")] real_linear_less2 1);
-by (Auto_tac);
+by Auto_tac;
 by (ftac DERIV_const_ratio_const2 1 THEN assume_tac 1);
 by (ftac DERIV_const_ratio_const2 2 THEN assume_tac 2);
 by (dtac real_less_half_sum 1);
diff -r 07f75bf77a33 -r c838477b5c18 src/HOL/Real/Hyperreal/Lim.thy
--- a/src/HOL/Real/Hyperreal/Lim.thy	Thu Dec 21 10:16:07 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Lim.thy	Thu Dec 21 10:16:33 2000 +0100
@@ -62,5 +62,18 @@
   isNSUCont :: (real=>real) => bool
   "isNSUCont f == (ALL x y. x @= y --> (*f* f) x @= (*f* f) y)"
 
+
+(*Used in the proof of the Bolzano theorem*)
+consts
+  Bolzano_bisect :: "[real*real=>bool, real, real, nat] => (real*real)"
+
+primrec
+  "Bolzano_bisect P a b 0 = (a,b)"
+  "Bolzano_bisect P a b (Suc n) =
+      (let (x,y) = Bolzano_bisect P a b n
+       in if P(x, (x+y)/#2) then ((x+y)/#2, y)
+                            else (x, (x+y)/#2) )"
+  
+
 end
 
diff -r 07f75bf77a33 -r c838477b5c18 src/HOL/Real/Hyperreal/NSA.ML
--- a/src/HOL/Real/Hyperreal/NSA.ML	Thu Dec 21 10:16:07 2000 +0100
+++ b/src/HOL/Real/Hyperreal/NSA.ML	Thu Dec 21 10:16:33 2000 +0100
@@ -32,7 +32,7 @@
 qed "SReal_inverse";
 
 Goalw [SReal_def] "x: SReal ==> -x : SReal";
-by (auto_tac (claset(), simpset() addsimps [hypreal_of_real_minus RS sym]));
+by (blast_tac (claset() addIs [hypreal_of_real_minus RS sym]) 1); 
 qed "SReal_minus";
 
 Goal "[| x + y : SReal; y: SReal |] ==> x: SReal";
@@ -220,7 +220,7 @@
 qed "HFinite_mult";
 
 Goalw [HFinite_def] "(x:HFinite)=(-x:HFinite)";
-by (simp_tac (simpset() addsimps [hrabs_minus_cancel]) 1);
+by (Simp_tac 1);
 qed "HFinite_minus_iff";
 
 Goal "[| x: HFinite; y: HFinite|] ==> (x + -y): HFinite";
@@ -298,7 +298,7 @@
 
 Goalw [Infinitesimal_def] 
      "(x:Infinitesimal) = (-x:Infinitesimal)";
-by (full_simp_tac (simpset() addsimps [hrabs_minus_cancel]) 1);
+by (Full_simp_tac 1);
 qed "Infinitesimal_minus_iff";
 
 Goal "x ~:Infinitesimal = (-x ~:Infinitesimal)";
@@ -389,8 +389,7 @@
 qed "HInfinite_add_gt_zero";
 
 Goalw [HInfinite_def] "(-x: HInfinite) = (x: HInfinite)";
-by (auto_tac (claset(),simpset() addsimps 
-    [hrabs_minus_cancel]));
+by Auto_tac;
 qed "HInfinite_minus_iff";
 
 Goal "[|x: HInfinite; y <= 0; x <= 0|] ==> (x + y): HInfinite";
@@ -592,7 +591,7 @@
 qed "inf_close_minus";
 
 Goal "-a @= -b ==> a @= b";
-by (auto_tac (claset() addDs [inf_close_minus],simpset()));
+by (auto_tac (claset() addDs [inf_close_minus], simpset()));
 qed "inf_close_minus2";
 
 Goal "(-a @= -b) = (a @= b)";
@@ -615,12 +614,6 @@
 by (asm_simp_tac (simpset() addsimps [inf_close_mult1,hypreal_mult_commute]) 1);
 qed "inf_close_mult2";
 
-val [prem1,prem2,prem3,prem4] = 
-goal thy "[|a @= b; c @= d; b: HFinite; c: HFinite|] ==> a*c @= b*d";
-by (fast_tac (claset() addIs [([prem1,prem4] MRS inf_close_mult1), 
-    ([prem2,prem3] MRS inf_close_mult2),inf_close_trans]) 1);
-qed "inf_close_mult_HFinite";
-
 Goal "[|u @= v*x; x @= y; v: HFinite|] ==> u @= v*y";
 by (fast_tac (claset() addIs [inf_close_mult2,inf_close_trans]) 1);
 qed "inf_close_mult_subst";
@@ -730,7 +723,7 @@
 by (dtac (bex_Infinitesimal_iff2 RS iffD2) 1);
 by (Step_tac 1);
 by (dtac (Infinitesimal_subset_HFinite RS subsetD 
-           RS (HFinite_minus_iff RS iffD1)) 1);
+          RS (HFinite_minus_iff RS iffD1)) 1);
 by (dtac HFinite_add 1);
 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
 qed "inf_close_HFinite";
@@ -740,10 +733,18 @@
 by Auto_tac;
 qed "inf_close_hypreal_of_real_HFinite";
 
+Goal "[|a @= b; c @= d; b: HFinite; d: HFinite|] ==> a*c @= b*d";
+by (rtac inf_close_trans 1); 
+by (rtac inf_close_mult2 2); 
+by (rtac inf_close_mult1 1);
+by (blast_tac (claset() addIs [inf_close_HFinite, inf_close_sym]) 2);  
+by Auto_tac;  
+qed "inf_close_mult_HFinite";
+
 Goal "[|a @= hypreal_of_real b; c @= hypreal_of_real d |] \
 \     ==> a*c @= hypreal_of_real b*hypreal_of_real d";
 by (blast_tac (claset() addSIs [inf_close_mult_HFinite,
-     inf_close_hypreal_of_real_HFinite,HFinite_hypreal_of_real]) 1);
+            inf_close_hypreal_of_real_HFinite,HFinite_hypreal_of_real]) 1);
 qed "inf_close_mult_hypreal_of_real";
 
 Goal "[| a: SReal; a ~= 0; a*x @= 0 |] ==> x @= 0";
@@ -886,7 +887,7 @@
 Goal "[| x @= y; y : HFinite - Infinitesimal |] \
 \     ==> x : HFinite - Infinitesimal";
 by (auto_tac (claset() addIs [inf_close_sym RSN (2,inf_close_HFinite)],
-    simpset() addsimps [mem_infmal_iff]));
+              simpset() addsimps [mem_infmal_iff]));
 by (dtac inf_close_trans3 1 THEN assume_tac 1);
 by (blast_tac (claset() addDs [inf_close_sym]) 1);
 qed "HFinite_diff_Infinitesimal_inf_close";
@@ -1457,12 +1458,14 @@
 by (dtac (hypreal_less_minus_iff RS iffD1) 1 THEN Step_tac 1);
 by (rtac (hypreal_less_minus_iff RS iffD2) 1);
 by (dres_inst_tac [("x","hypreal_of_real y + -hypreal_of_real x")] bspec 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_add_commute,
-    hypreal_of_real_minus RS sym, hypreal_of_real_add RS sym,
-    hrabs_interval_iff]));
+by (auto_tac (claset(),
+              simpset() addsimps [hypreal_add_commute, 
+                                  hypreal_of_real_add, hrabs_interval_iff,
+                                  SReal_add, SReal_minus]));
 by (dres_inst_tac [("x1","xa")] (hypreal_less_minus_iff RS iffD1) 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_minus,
-    hypreal_minus_add_distrib,hypreal_of_real_add] @ hypreal_add_ac));
+by (auto_tac (claset(),
+        simpset() addsimps [hypreal_minus_add_distrib,hypreal_of_real_add] @ 
+                           hypreal_add_ac));
 qed "Infinitesimal_add_hypreal_of_real_less";
 
 Goal "[| x: Infinitesimal; abs(hypreal_of_real r) < hypreal_of_real y |] \
@@ -2241,12 +2244,14 @@
  -----------------------------------------------------*)
 Goal "ALL n. abs(X n + -x) < inverse(real_of_posnat n) \ 
 \    ==> Abs_hypreal(hyprel^^{X}) + -hypreal_of_real x : Infinitesimal";
-by (auto_tac (claset() addSIs [bexI] addDs [rename_numerals 
-    FreeUltrafilterNat_inverse_real_of_posnat,
-    FreeUltrafilterNat_all,FreeUltrafilterNat_Int] addIs [order_less_trans,
-    FreeUltrafilterNat_subset],simpset() addsimps [hypreal_minus,
-    hypreal_of_real_minus RS sym,hypreal_of_real_def,hypreal_add,
-    Infinitesimal_FreeUltrafilterNat_iff,hypreal_inverse,hypreal_of_real_of_posnat]));
+by (auto_tac (claset() addSIs [bexI] 
+           addDs [rename_numerals FreeUltrafilterNat_inverse_real_of_posnat,
+                  FreeUltrafilterNat_all,FreeUltrafilterNat_Int] 
+           addIs [order_less_trans, FreeUltrafilterNat_subset],
+      simpset() addsimps [hypreal_minus, 
+                          hypreal_of_real_def,hypreal_add,
+                          Infinitesimal_FreeUltrafilterNat_iff,hypreal_inverse,
+                          hypreal_of_real_of_posnat]));
 qed "real_seq_to_hypreal_Infinitesimal";
 
 Goal "ALL n. abs(X n + -x) < inverse(real_of_posnat n) \ 
@@ -2274,4 +2279,3 @@
             [Infinitesimal_FreeUltrafilterNat_iff,hypreal_minus,hypreal_add, 
              hypreal_inverse,hypreal_of_real_of_posnat]));
 qed "real_seq_to_hypreal_Infinitesimal2";
- 
\ No newline at end of file
diff -r 07f75bf77a33 -r c838477b5c18 src/HOL/Real/Hyperreal/NatStar.ML
--- a/src/HOL/Real/Hyperreal/NatStar.ML	Thu Dec 21 10:16:07 2000 +0100
+++ b/src/HOL/Real/Hyperreal/NatStar.ML	Thu Dec 21 10:16:33 2000 +0100
@@ -8,16 +8,14 @@
 
 Goalw [starsetNat_def] 
       "*sNat*(UNIV::nat set) = (UNIV::hypnat set)";
-by (auto_tac (claset(),simpset() addsimps 
-    [FreeUltrafilterNat_Nat_set]));
+by (auto_tac (claset(), simpset() addsimps [FreeUltrafilterNat_Nat_set]));
 qed "NatStar_real_set";
 
 Goalw [starsetNat_def] "*sNat* {} = {}";
 by (Step_tac 1);
 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
 by (dres_inst_tac [("x","%n. xa n")] bspec 1);
-by (auto_tac (claset(),simpset() addsimps 
-    [FreeUltrafilterNat_empty]));
+by (auto_tac (claset(), simpset() addsimps [FreeUltrafilterNat_empty]));
 qed "NatStar_empty_set";
 
 Addsimps [NatStar_empty_set];
@@ -25,8 +23,7 @@
 Goalw [starsetNat_def] 
       "*sNat* (A Un B) = *sNat* A Un *sNat* B";
 by (Auto_tac);
-by (REPEAT(blast_tac (claset() addIs 
-   [FreeUltrafilterNat_subset]) 2));
+by (REPEAT(blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 2));
 by (dtac FreeUltrafilterNat_Compl_mem 1);
 by (dtac bspec 1 THEN assume_tac 1);
 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
@@ -39,14 +36,15 @@
 by Auto_tac;
 by (dres_inst_tac [("x","Xa")] bspec 1);
 by (res_inst_tac [("z","x")] eq_Abs_hypnat 2);
-by (auto_tac (claset() addSDs [bspec],simpset()));
+by (auto_tac (claset() addSDs [bspec], simpset()));
 by (TRYALL(Ultra_tac));
 qed "starsetNat_n_Un";
 
 Goalw [InternalNatSets_def]
      "[| X : InternalNatSets; Y : InternalNatSets |] \
 \     ==> (X Un Y) : InternalNatSets";
-by (auto_tac (claset(),simpset() addsimps [starsetNat_n_Un RS sym]));
+by (auto_tac (claset(),
+         simpset() addsimps [starsetNat_n_Un RS sym]));
 qed "InternalNatSets_Un";
 
 Goalw [starsetNat_def] "*sNat* (A Int B) = *sNat* A Int *sNat* B";
@@ -60,14 +58,16 @@
 Goalw [starsetNat_n_def] 
       "*sNatn* (%n. (A n) Int (B n)) = *sNatn* A Int *sNatn* B";
 by (Auto_tac);
-by (auto_tac (claset() addSDs [bspec],simpset()));
+by (auto_tac (claset() addSDs [bspec],
+         simpset()));
 by (TRYALL(Ultra_tac));
 qed "starsetNat_n_Int";
 
 Goalw [InternalNatSets_def]
      "[| X : InternalNatSets; Y : InternalNatSets |] \
 \     ==> (X Int Y) : InternalNatSets";
-by (auto_tac (claset(),simpset() addsimps [starsetNat_n_Int RS sym]));
+by (auto_tac (claset(),
+         simpset() addsimps [starsetNat_n_Int RS sym]));
 qed "InternalNatSets_Int";
 
 Goalw [starsetNat_def] "*sNat* (-A) = -(*sNat* A)";
@@ -88,7 +88,8 @@
 
 Goalw [InternalNatSets_def]
      "X :InternalNatSets ==> -X : InternalNatSets";
-by (auto_tac (claset(),simpset() addsimps [starsetNat_n_Compl RS sym]));
+by (auto_tac (claset(),
+         simpset() addsimps [starsetNat_n_Compl RS sym]));
 qed "InternalNatSets_Compl";
 
 Goalw [starsetNat_n_def] 
@@ -96,27 +97,28 @@
 by (Auto_tac);
 by (res_inst_tac [("z","x")] eq_Abs_hypnat 2);
 by (res_inst_tac [("z","x")] eq_Abs_hypnat 3);
-by (auto_tac (claset() addSDs [bspec],simpset()));
+by (auto_tac (claset() addSDs [bspec], simpset()));
 by (TRYALL(Ultra_tac));
 qed "starsetNat_n_diff";
 
 Goalw [InternalNatSets_def]
      "[| X : InternalNatSets; Y : InternalNatSets |] \
 \     ==> (X - Y) : InternalNatSets";
-by (auto_tac (claset(),simpset() addsimps [starsetNat_n_diff RS sym]));
+by (auto_tac (claset(), simpset() addsimps [starsetNat_n_diff RS sym]));
 qed "InternalNatSets_diff";
 
-Goalw [starsetNat_def] "!!A. A <= B ==> *sNat* A <= *sNat* B";
+Goalw [starsetNat_def] "A <= B ==> *sNat* A <= *sNat* B";
 by (REPEAT(blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1));
 qed "NatStar_subset";
 
 Goalw [starsetNat_def,hypnat_of_nat_def] 
-          "!!A. a : A ==> hypnat_of_nat a : *sNat* A";
-by (auto_tac (claset() addIs [FreeUltrafilterNat_subset],simpset()));
+          "a : A ==> hypnat_of_nat a : *sNat* A";
+by (auto_tac (claset() addIs [FreeUltrafilterNat_subset],
+         simpset()));
 qed "NatStar_mem";
 
 Goalw [starsetNat_def] "hypnat_of_nat `` A <= *sNat* A";
-by (auto_tac (claset(),simpset() addsimps [hypnat_of_nat_def]));
+by (auto_tac (claset(), simpset() addsimps [hypnat_of_nat_def]));
 by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1);
 qed "NatStar_hypreal_of_real_image_subset";
 
@@ -127,7 +129,8 @@
 
 Goalw [starsetNat_def] 
       "*sNat* X Int SHNat = hypnat_of_nat `` X";
-by (auto_tac (claset(),simpset() addsimps 
+by (auto_tac (claset(),
+         simpset() addsimps 
            [hypnat_of_nat_def,SHNat_def]));
 by (fold_tac [hypnat_of_nat_def]);
 by (rtac imageI 1 THEN rtac ccontr 1);
@@ -137,7 +140,7 @@
 by (Auto_tac);
 qed "NatStar_hypreal_of_real_Int";
 
-Goal "!!x. x ~: hypnat_of_nat `` A ==> ALL y: A. x ~= hypnat_of_nat y";
+Goal "x ~: hypnat_of_nat `` A ==> ALL y: A. x ~= hypnat_of_nat y";
 by (Auto_tac);
 qed "lemma_not_hypnatA";
 
@@ -146,12 +149,13 @@
 qed "starsetNat_starsetNat_n_eq";
 
 Goalw [InternalNatSets_def] "(*sNat* X) : InternalNatSets";
-by (auto_tac (claset(),simpset() addsimps [starsetNat_starsetNat_n_eq]));
+by (auto_tac (claset(),
+         simpset() addsimps [starsetNat_starsetNat_n_eq]));
 qed "InternalNatSets_starsetNat_n";
 Addsimps [InternalNatSets_starsetNat_n];
 
 Goal "X : InternalNatSets ==> UNIV - X : InternalNatSets";
-by (auto_tac (claset() addIs [InternalNatSets_Compl],simpset()));
+by (auto_tac (claset() addIs [InternalNatSets_Compl], simpset()));
 qed "InternalNatSets_UNIV_diff";
 
 (*------------------------------------------------------------------ 
@@ -160,7 +164,7 @@
  -----------------------------------------------------------------*)
 
 Goalw [starsetNat_n_def,starsetNat_def] 
-     "!!A. ALL n. (As n = A) ==> *sNatn* As = *sNat* A";
+     "ALL n. (As n = A) ==> *sNatn* As = *sNat* A";
 by (Auto_tac);
 qed "starsetNat_n_starsetNat";
 
@@ -174,12 +178,12 @@
  -----------------------------------------------------------------*)
 
 Goalw [starfunNat_n_def,starfunNat_def] 
-     "!!A. ALL n. (F n = f) ==> *fNatn* F = *fNat* f";
+     "ALL n. (F n = f) ==> *fNatn* F = *fNat* f";
 by (Auto_tac);
 qed "starfunNat_n_starfunNat";
 
 Goalw [starfunNat2_n_def,starfunNat2_def] 
-     "!!A. ALL n. (F n = f) ==> *fNat2n* F = *fNat2* f";
+     "ALL n. (F n = f) ==> *fNat2n* F = *fNat2* f";
 by (Auto_tac);
 qed "starfunNat2_n_starfunNat2";
 
@@ -214,14 +218,12 @@
  ---------------------------------------------*)
 Goal "(*fNat* f) xa * (*fNat* g) xa = (*fNat* (%x. f x * g x)) xa";
 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps 
-    [starfunNat,hypreal_mult]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat,hypreal_mult]));
 qed "starfunNat_mult";
 
 Goal "(*fNat2* f) xa * (*fNat2* g) xa = (*fNat2* (%x. f x * g x)) xa";
 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps 
-    [starfunNat2,hypnat_mult]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_mult]));
 qed "starfunNat2_mult";
 
 (*---------------------------------------
@@ -229,29 +231,17 @@
  ---------------------------------------*)
 Goal "(*fNat* f) xa + (*fNat* g) xa = (*fNat* (%x. f x + g x)) xa";
 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps 
-    [starfunNat,hypreal_add]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat,hypreal_add]));
 qed "starfunNat_add";
 
 Goal "(*fNat2* f) xa + (*fNat2* g) xa = (*fNat2* (%x. f x + g x)) xa";
 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps 
-    [starfunNat2,hypnat_add]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_add]));
 qed "starfunNat2_add";
 
-(*--------------------------------------------
-  subtraction: ( *f ) + -( *g ) = *(f + -g)  
- --------------------------------------------*)
-Goal "(*fNat* f) xa + -(*fNat* g) xa = (*fNat* (%x. f x + -g x)) xa";
-by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat,
-    hypreal_minus,hypreal_add]));
-qed "starfunNat_add_minus";
-
 Goal "(*fNat2* f) xa - (*fNat2* g) xa = (*fNat2* (%x. f x - g x)) xa";
 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat2,
-    hypnat_minus]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat2, hypnat_minus]));
 qed "starfunNat2_minus";
 
 (*--------------------------------------
@@ -262,8 +252,7 @@
 Goal "(*fNat* f) o (*fNat2* g) = (*fNat* (f o g))";
 by (rtac ext 1);
 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat2,
-    starfunNat]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat2, starfunNat]));
 qed "starfunNatNat2_o";
 
 Goal "(%x. (*fNat* f) ((*fNat2* g) x)) = (*fNat* (%x. f(g x)))";
@@ -274,7 +263,7 @@
 Goal "(*fNat2* f) o (*fNat2* g) = (*fNat2* (f o g))";
 by (rtac ext 1);
 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat2]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat2]));
 qed "starfunNat2_o";
 
 (***** ( *f::real=>real ) o ( *g::nat=>real ) = *(f o g) *****)
@@ -282,7 +271,7 @@
 Goal "(*f* f) o (*fNat* g) = (*fNat* (f o g))"; 
 by (rtac ext 1);
 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat,starfun]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat,starfun]));
 qed "starfun_stafunNat_o";
 
 Goal "(%x. (*f* f) ((*fNat* g) x)) = (*fNat* (%x. f (g x)))"; 
@@ -294,23 +283,20 @@
  --------------------------------------*)
 Goal "(*fNat* (%x. k)) xa = hypreal_of_real k";
 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat,
-    hypreal_of_real_def]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_of_real_def]));
 qed "starfunNat_const_fun";
 Addsimps [starfunNat_const_fun];
 
 Goal "(*fNat2* (%x. k)) xa = hypnat_of_nat  k";
 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat2,
-    hypnat_of_nat_def]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat2, hypnat_of_nat_def]));
 qed "starfunNat2_const_fun";
 
 Addsimps [starfunNat2_const_fun];
 
 Goal "- (*fNat* f) x = (*fNat* (%x. - f x)) x";
 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat,
-              hypreal_minus]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_minus]));
 qed "starfunNat_minus";
 
 Goal "inverse ((*fNat* f) x) = (*fNat* (%x. inverse (f x))) x";
@@ -325,15 +311,14 @@
  -------------------------------------------------------*)
 
 Goal "(*fNat* f) (hypnat_of_nat a) = hypreal_of_real (f a)";
-by (auto_tac (claset(),simpset() addsimps 
-     [starfunNat,hypnat_of_nat_def,hypreal_of_real_def]));
+by (auto_tac (claset(),
+      simpset() addsimps [starfunNat,hypnat_of_nat_def,hypreal_of_real_def]));
 qed "starfunNat_eq";
 
 Addsimps [starfunNat_eq];
 
 Goal "(*fNat2* f) (hypnat_of_nat a) = hypnat_of_nat (f a)";
-by (auto_tac (claset(),simpset() addsimps 
-     [starfunNat2,hypnat_of_nat_def]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_of_nat_def]));
 qed "starfunNat2_eq";
 
 Addsimps [starfunNat2_eq];
@@ -342,46 +327,30 @@
 by (Auto_tac);
 qed "starfunNat_inf_close";
 
-Goal "!!f. [| (*fNat* f) xa @= l; (*fNat* g) xa @= m; \
-\                 l: HFinite; m: HFinite  \
-\              |] ==>  (*fNat* (%x. f x * g x)) xa @= l * m";
-by (dtac inf_close_mult_HFinite 1);
-by (REPEAT(assume_tac 1));
-by (auto_tac (claset() addIs [inf_close_sym RSN (2,inf_close_HFinite)],
-              simpset() addsimps [starfunNat_mult]));
-qed "starfunNat_mult_HFinite_inf_close";
-
-Goal "!!f. [| (*fNat* f) xa @= l; (*fNat* g) xa @= m \
-\              |] ==>  (*fNat* (%x. f x + g x)) xa @= l + m";
-by (auto_tac (claset() addIs [inf_close_add],
-              simpset() addsimps [starfunNat_add RS sym]));
-qed "starfunNat_add_inf_close";
-
 
 (*-----------------------------------------------------------------
     Example of transfer of a property from reals to hyperreals
     --- used for limit comparison of sequences
  ----------------------------------------------------------------*)
-Goal "!!f. ALL n. N <= n --> f n <= g n \
+Goal "ALL n. N <= n --> f n <= g n \
 \         ==> ALL n. hypnat_of_nat N <= n --> (*fNat* f) n <= (*fNat* g) n";
 by (Step_tac 1);
 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat,
-        hypnat_of_nat_def,hypreal_le,hypreal_less,
-        hypnat_le,hypnat_less]));
+by (auto_tac (claset(),
+         simpset() addsimps [starfunNat, hypnat_of_nat_def,hypreal_le,
+                             hypreal_less, hypnat_le,hypnat_less]));
 by (Ultra_tac 1);
 by Auto_tac;
 qed "starfun_le_mono";
 
 (*****----- and another -----*****) 
-goal NatStar.thy 
-     "!!f. ALL n. N <= n --> f n < g n \
+Goal "ALL n. N <= n --> f n < g n \
 \         ==> ALL n. hypnat_of_nat N <= n --> (*fNat* f) n < (*fNat* g) n";
 by (Step_tac 1);
 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat,
-        hypnat_of_nat_def,hypreal_le,hypreal_less,
-        hypnat_le,hypnat_less]));
+by (auto_tac (claset(),
+         simpset() addsimps [starfunNat, hypnat_of_nat_def,hypreal_le,
+                             hypreal_less, hypnat_le,hypnat_less]));
 by (Ultra_tac 1);
 by Auto_tac;
 qed "starfun_less_mono";
@@ -391,8 +360,8 @@
  ---------------------------------------------------------------*)
 Goal "(*fNat* (%n. f (Suc n))) N = (*fNat* f) (N + 1hn)";
 by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat,
-    hypnat_one_def,hypnat_add]));
+by (auto_tac (claset(),
+         simpset() addsimps [starfunNat, hypnat_one_def,hypnat_add]));
 qed "starfunNat_shift_one";
 
 (*----------------------------------------------------------------
@@ -400,8 +369,7 @@
  ---------------------------------------------------------------*)
 Goal "(*fNat* (%n. abs (f n))) N = abs((*fNat* f) N)";
 by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat,
-    hypreal_hrabs]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_hrabs]));
 qed "starfunNat_rabs";
 
 (*----------------------------------------------------------------
@@ -409,19 +377,19 @@
  ----------------------------------------------------------------*)
 Goal "(*fNat* (%n. r ^ n)) N = (hypreal_of_real r) pow N";
 by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [hyperpow,
-    hypreal_of_real_def,starfunNat]));
+by (auto_tac (claset(),
+         simpset() addsimps [hyperpow, hypreal_of_real_def,starfunNat]));
 qed "starfunNat_pow";
 
 Goal "(*fNat* (%n. (X n) ^ m)) N = (*fNat* X) N pow hypnat_of_nat m";
 by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [hyperpow,
-    hypnat_of_nat_def,starfunNat]));
+by (auto_tac (claset(),
+         simpset() addsimps [hyperpow, hypnat_of_nat_def,starfunNat]));
 qed "starfunNat_pow2";
 
 Goalw [hypnat_of_nat_def] "(*f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n";
 by (res_inst_tac [("z","R")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hyperpow,starfun]));
+by (auto_tac (claset(), simpset() addsimps [hyperpow,starfun]));
 qed "starfun_pow";
 
 (*----------------------------------------------------- 
@@ -430,15 +398,15 @@
 Goal "(*fNat* real_of_nat) = hypreal_of_hypnat";
 by (rtac ext 1);
 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_of_hypnat,starfunNat]));
+by (auto_tac (claset(), simpset() addsimps [hypreal_of_hypnat,starfunNat]));
 qed "starfunNat_real_of_nat";
 
 Goal "N : HNatInfinite \
 \     ==> (*fNat* (%x. inverse (real_of_nat x))) N = inverse(hypreal_of_hypnat N)";
 by (res_inst_tac [("f1","inverse")]  (starfun_stafunNat_o2 RS subst) 1);
 by (subgoal_tac "hypreal_of_hypnat N ~= 0" 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat_real_of_nat, 
-    starfun_inverse_inverse]));
+by (auto_tac (claset(), 
+       simpset() addsimps [starfunNat_real_of_nat, starfun_inverse_inverse]));
 qed "starfunNat_inverse_real_of_nat_eq";
 
 (*----------------------------------------------------------
@@ -464,8 +432,7 @@
 Goal "(*fNatn* f) xa * (*fNatn* g) xa = \
 \         (*fNatn* (% i x. f i x * g i x)) xa";
 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps 
-    [starfunNat_n,hypreal_mult]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypreal_mult]));
 qed "starfunNat_n_mult";
 
 (*-----------------------------------------------
@@ -474,8 +441,7 @@
 Goal "(*fNatn* f) xa + (*fNatn* g) xa = \
 \         (*fNatn* (%i x. f i x + g i x)) xa";
 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps 
-    [starfunNat_n,hypreal_add]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypreal_add]));
 qed "starfunNat_n_add";
 
 (*-------------------------------------------------
@@ -484,8 +450,8 @@
 Goal "(*fNatn* f) xa + -(*fNatn* g) xa = \
 \         (*fNatn* (%i x. f i x + -g i x)) xa";
 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat_n,
-    hypreal_minus,hypreal_add]));
+by (auto_tac (claset(), 
+          simpset() addsimps [starfunNat_n, hypreal_minus,hypreal_add]));
 qed "starfunNat_n_add_minus";
 
 (*--------------------------------------------------
@@ -494,22 +460,20 @@
  
 Goal "(*fNatn* (%i x. k)) xa = hypreal_of_real  k";
 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat_n,
-    hypreal_of_real_def]));
+by (auto_tac (claset(), 
+       simpset() addsimps [starfunNat_n, hypreal_of_real_def]));
 qed "starfunNat_n_const_fun";
 
 Addsimps [starfunNat_n_const_fun];
 
 Goal "- (*fNatn* f) x = (*fNatn* (%i x. - (f i) x)) x";
 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat_n,
-              hypreal_minus]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat_n, hypreal_minus]));
 qed "starfunNat_n_minus";
 
 Goal "(*fNatn* f) (hypnat_of_nat n) = \
 \         Abs_hypreal(hyprel ^^ {%i. f i n})";
-by (auto_tac (claset(),simpset() addsimps 
-     [starfunNat_n,hypnat_of_nat_def]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypnat_of_nat_def]));
 qed "starfunNat_n_eq";
 Addsimps [starfunNat_n_eq];
 
@@ -517,7 +481,7 @@
 by Auto_tac;
 by (rtac ext 1 THEN rtac ccontr 1);
 by (dres_inst_tac [("x","hypnat_of_nat(x)")] fun_cong 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat,hypnat_of_nat_def]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat,hypnat_of_nat_def]));
 qed "starfun_eq_iff";
 
 
diff -r 07f75bf77a33 -r c838477b5c18 src/HOL/Real/Hyperreal/SEQ.ML
--- a/src/HOL/Real/Hyperreal/SEQ.ML	Thu Dec 21 10:16:07 2000 +0100
+++ b/src/HOL/Real/Hyperreal/SEQ.ML	Thu Dec 21 10:16:33 2000 +0100
@@ -208,16 +208,15 @@
     simpset() addsimps [starfunNat_add RS sym,hypreal_of_real_add]));
 qed "NSLIMSEQ_add";
 
-Goal "[| X ----> a; Y ----> b |] \
-\           ==> (%n. X n + Y n) ----> a + b";
+Goal "[| X ----> a; Y ----> b |] ==> (%n. X n + Y n) ----> a + b";
 by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
     NSLIMSEQ_add]) 1);
 qed "LIMSEQ_add";
 
 Goalw [NSLIMSEQ_def]
       "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b";
-by (auto_tac (claset() addSIs [starfunNat_mult_HFinite_inf_close],
-    simpset() addsimps [hypreal_of_real_mult]));
+by (auto_tac (claset() addSIs [inf_close_mult_HFinite],
+    simpset() addsimps [hypreal_of_real_mult, starfunNat_mult RS sym]));
 qed "NSLIMSEQ_mult";
 
 Goal "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b";
@@ -227,8 +226,7 @@
 
 Goalw [NSLIMSEQ_def] 
      "X ----NS> a ==> (%n. -(X n)) ----NS> -a";
-by (auto_tac (claset() addIs [inf_close_minus],
-       simpset() addsimps [starfunNat_minus RS sym, hypreal_of_real_minus]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat_minus RS sym]));
 qed "NSLIMSEQ_minus";
 
 Goal "X ----> a ==> (%n. -(X n)) ----> -a";
@@ -756,14 +754,13 @@
 qed "convergent_minus_iff";
 
 Goalw [Bseq_def] "Bseq (%n. -(X n)) = Bseq X";
-by (asm_full_simp_tac (simpset() addsimps [abs_minus_cancel]) 1);
+by (Asm_full_simp_tac 1);
 qed "Bseq_minus_iff";
 
 (*--------------------------------
    **** main mono theorem ****
  -------------------------------*)
-Goalw [monoseq_def] 
-      "[| Bseq X; monoseq X |] ==> convergent X";
+Goalw [monoseq_def] "[| Bseq X; monoseq X |] ==> convergent X";
 by (Step_tac 1);
 by (rtac (convergent_minus_iff RS ssubst) 2);
 by (dtac (Bseq_minus_iff RS ssubst) 2);
diff -r 07f75bf77a33 -r c838477b5c18 src/HOL/Real/Hyperreal/Star.ML
--- a/src/HOL/Real/Hyperreal/Star.ML	Thu Dec 21 10:16:07 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Star.ML	Thu Dec 21 10:16:33 2000 +0100
@@ -212,6 +212,7 @@
 by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1);
 by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_mult]));
 qed "starfun_mult";
+Addsimps [starfun_mult RS sym];
 
 (*---------------------------------------
   addition: ( *f ) + ( *g ) = *(f + g)  
@@ -220,6 +221,7 @@
 by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1);
 by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_add]));
 qed "starfun_add";
+Addsimps [starfun_add RS sym];
 
 (*--------------------------------------------
   subtraction: ( *f ) + -( *g ) = *(f + -g)  
@@ -229,21 +231,25 @@
 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
 by (auto_tac (claset(),simpset() addsimps [starfun, hypreal_minus]));
 qed "starfun_minus";
+Addsimps [starfun_minus RS sym];
 
+(*FIXME: delete*)
 Goal "(*f* f) xa + -(*f* g) xa = (*f* (%x. f x + -g x)) xa";
-by (simp_tac (simpset() addsimps [starfun_minus, starfun_add]) 1);
+by (Simp_tac 1);
 qed "starfun_add_minus";
+Addsimps [starfun_add_minus RS sym];
 
 Goalw [hypreal_diff_def,real_diff_def]
   "(*f* f) xa  - (*f* g) xa = (*f* (%x. f x - g x)) xa";
 by (rtac starfun_add_minus 1);
 qed "starfun_diff";
+Addsimps [starfun_diff RS sym];
 
 (*--------------------------------------
   composition: ( *f ) o ( *g ) = *(f o g)  
  ---------------------------------------*)
 
-Goal "(%x. (*f* f) ((*f* g) x)) = *f* (%x. f (g x))";
+Goal "(%x. (*f* f) ((*f* g) x)) = *f* (%x. f (g x))"; 
 by (rtac ext 1);
 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
 by (auto_tac (claset(),simpset() addsimps [starfun]));
@@ -343,13 +349,12 @@
 by (dtac inf_close_mult_HFinite 1);
 by (REPEAT(assume_tac 1));
 by (auto_tac (claset() addIs [inf_close_sym RSN (2,inf_close_HFinite)],
-              simpset() addsimps [starfun_mult]));
+              simpset()));
 qed "starfun_mult_HFinite_inf_close";
 
 Goal "[| (*f* f) xa @= l; (*f* g) xa @= m \
 \              |] ==>  (*f* (%x. f x + g x)) xa @= l + m";
-by (auto_tac (claset() addIs [inf_close_add],
-              simpset() addsimps [starfun_add RS sym]));
+by (auto_tac (claset() addIs [inf_close_add], simpset()));
 qed "starfun_add_inf_close";
 
 (*----------------------------------------------------
@@ -363,7 +368,7 @@
 
 Goal "*f* abs = abs";
 by (rtac (hrabs_is_starext_rabs RS 
-    (is_starext_starfun_iff RS iffD1) RS sym) 1);
+          (is_starext_starfun_iff RS iffD1) RS sym) 1);
 qed "starfun_rabs_hrabs";
 
 Goal "(*f* inverse) x = inverse(x)";
@@ -382,11 +387,13 @@
 by (auto_tac (claset(),
               simpset() addsimps [starfun, hypreal_inverse]));
 qed "starfun_inverse";
+Addsimps [starfun_inverse RS sym];
 
 Goalw [hypreal_divide_def,real_divide_def]
   "(*f* f) xa  / (*f* g) xa = (*f* (%x. f x / g x)) xa";
-by (simp_tac (simpset() addsimps [starfun_inverse, starfun_mult]) 1);
+by Auto_tac;
 qed "starfun_divide";
+Addsimps [starfun_divide RS sym];
 
 Goal "inverse ((*f* f) x) = (*f* (%x. inverse (f x))) x";
 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
@@ -424,12 +431,13 @@
    by its NS extenson ( *f* f). See second NS set extension below.
  ----------------------------------------------------------------*)
 Goalw [starset_def]
-   "*s* {x. abs (x + - y) < r} = {x. abs(x + -hypreal_of_real y) < hypreal_of_real r}";
+   "*s* {x. abs (x + - y) < r} = \
+\    {x. abs(x + -hypreal_of_real y) < hypreal_of_real r}";
 by (Step_tac 1);
 by (ALLGOALS(res_inst_tac [("z","x")] eq_Abs_hypreal));
 by (auto_tac (claset() addSIs [exI] addSDs [bspec],
-    simpset() addsimps [hypreal_minus, hypreal_of_real_def,hypreal_add,
-    hypreal_hrabs,hypreal_less_def]));
+          simpset() addsimps [hypreal_minus, hypreal_of_real_def,hypreal_add,
+                              hypreal_hrabs,hypreal_less_def]));
 by (Fuf_tac 1);
 qed "STAR_rabs_add_minus";
 
diff -r 07f75bf77a33 -r c838477b5c18 src/HOL/Real/RealAbs.ML
--- a/src/HOL/Real/RealAbs.ML	Thu Dec 21 10:16:07 2000 +0100
+++ b/src/HOL/Real/RealAbs.ML	Thu Dec 21 10:16:33 2000 +0100
@@ -8,7 +8,7 @@
 
 (** abs (absolute value) **)
 
-Goalw [abs_real_def]
+Goalw [real_abs_def]
      "abs (number_of v :: real) = \
 \       (if neg (number_of v) then number_of (bin_minus v) \
 \        else number_of v)";
@@ -21,7 +21,7 @@
 
 Addsimps [abs_nat_number_of];
 
-Goalw [abs_real_def]
+Goalw [real_abs_def]
   "P(abs (x::real)) = ((#0 <= x --> P x) & (x < #0 --> P(-x)))";
 by(auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0]));
 qed "abs_split";
@@ -32,63 +32,63 @@
        (adapted version of previously proved theorems about abs)
  ----------------------------------------------------------------------------*)
 
-Goalw [abs_real_def] "abs (r::real) = (if #0<=r then r else -r)";
+Goalw [real_abs_def] "abs (r::real) = (if #0<=r then r else -r)";
 by Auto_tac;
 qed "abs_iff";
 
-Goalw [abs_real_def] "abs #0 = (#0::real)";
+Goalw [real_abs_def] "abs #0 = (#0::real)";
 by Auto_tac;
 qed "abs_zero";
 Addsimps [abs_zero];
 
-Goalw [abs_real_def] "abs (#0::real) = -#0";
+Goalw [real_abs_def] "abs (#0::real) = -#0";
 by (Simp_tac 1);
 qed "abs_minus_zero";
 
-Goalw [abs_real_def] "(#0::real)<=x ==> abs x = x";
+Goalw [real_abs_def] "(#0::real)<=x ==> abs x = x";
 by (Asm_simp_tac 1);
 qed "abs_eqI1";
 
-Goalw [abs_real_def] "(#0::real)<x ==> abs x = x";
+Goalw [real_abs_def] "(#0::real)<x ==> abs x = x";
 by (Asm_simp_tac 1);
 qed "abs_eqI2";
 
-Goalw [abs_real_def,real_le_def] "x<(#0::real) ==> abs x = -x";
+Goalw [real_abs_def,real_le_def] "x<(#0::real) ==> abs x = -x";
 by (Asm_simp_tac 1);
 qed "abs_minus_eqI2";
 
-Goalw [abs_real_def] "x<=(#0::real) ==> abs x = -x";
+Goalw [real_abs_def] "x<=(#0::real) ==> abs x = -x";
 by (Asm_simp_tac 1);
 qed "abs_minus_eqI1";
 
-Goalw [abs_real_def] "(#0::real)<= abs x";
+Goalw [real_abs_def] "(#0::real)<= abs x";
 by (Simp_tac 1);
 qed "abs_ge_zero";
 
-Goalw [abs_real_def] "abs(abs x)=abs (x::real)";
+Goalw [real_abs_def] "abs(abs x)=abs (x::real)";
 by (Simp_tac 1);
 qed "abs_idempotent";
 Addsimps [abs_idempotent];
 
-Goalw [abs_real_def] "(abs x = #0) = (x=(#0::real))";
+Goalw [real_abs_def] "(abs x = #0) = (x=(#0::real))";
 by (Full_simp_tac 1);
 qed "abs_zero_iff";
 AddIffs [abs_zero_iff];
 
-Goalw [abs_real_def] "x<=abs (x::real)";
+Goalw [real_abs_def] "x<=abs (x::real)";
 by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
 qed "abs_ge_self";
 
-Goalw [abs_real_def] "-x<=abs (x::real)";
+Goalw [real_abs_def] "-x<=abs (x::real)";
 by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
 qed "abs_ge_minus_self";
 
-Goalw [abs_real_def] "abs (x * y) = abs x * abs (y::real)";
+Goalw [real_abs_def] "abs (x * y) = abs x * abs (y::real)";
 by (auto_tac (claset() addSDs [order_antisym],
 	      simpset() addsimps [real_0_le_mult_iff]));
 qed "abs_mult";
 
-Goalw [abs_real_def] "abs(inverse(x::real)) = inverse(abs(x))";
+Goalw [real_abs_def] "abs(inverse(x::real)) = inverse(abs(x))";
 by (real_div_undefined_case_tac "x=0" 1);
 by (auto_tac (claset(), 
               simpset() addsimps [real_minus_inverse, real_le_less] @ 
@@ -99,7 +99,7 @@
 by (asm_simp_tac (simpset() addsimps [abs_mult, abs_inverse]) 1);
 qed "abs_mult_inverse";
 
-Goalw [abs_real_def] "abs(x+y) <= abs x + abs (y::real)";
+Goalw [real_abs_def] "abs(x+y) <= abs x + abs (y::real)";
 by (Simp_tac 1);
 qed "abs_triangle_ineq";
 
@@ -108,23 +108,24 @@
 by (simp_tac (simpset() addsimps [abs_triangle_ineq RS order_trans]) 1);
 qed "abs_triangle_ineq_four";
 
-Goalw [abs_real_def] "abs(-x)=abs(x::real)";
+Goalw [real_abs_def] "abs(-x)=abs(x::real)";
 by (Simp_tac 1);
 qed "abs_minus_cancel";
+Addsimps [abs_minus_cancel];
 
-Goalw [abs_real_def] "abs(x + (-y)) = abs (y + (-(x::real)))";
+Goalw [real_abs_def] "abs(x + (-y)) = abs (y + (-(x::real)))";
 by (Simp_tac 1);
 qed "abs_minus_add_cancel";
 
-Goalw [abs_real_def] "abs(x + (-y)) <= abs x + abs (y::real)";
+Goalw [real_abs_def] "abs(x + (-y)) <= abs x + abs (y::real)";
 by (Simp_tac 1);
 qed "abs_triangle_minus_ineq";
 
-Goalw [abs_real_def] "abs x < r --> abs y < s --> abs(x+y) < r+(s::real)";
+Goalw [real_abs_def] "abs x < r --> abs y < s --> abs(x+y) < r+(s::real)";
 by (Simp_tac 1);
 qed_spec_mp "abs_add_less";
 
-Goalw [abs_real_def] "abs x < r --> abs y < s --> abs(x+ (-y)) < r+(s::real)";
+Goalw [real_abs_def] "abs x < r --> abs y < s --> abs(x+ (-y)) < r+(s::real)";
 by (Simp_tac 1);
 qed "abs_add_minus_less";
 
@@ -181,42 +182,38 @@
 by (blast_tac (claset() addSIs [real_le_less_trans,abs_ge_zero]) 1);
 qed "abs_less_gt_zero";
 
-Goalw [abs_real_def] "abs #1 = (#1::real)";
+Goalw [real_abs_def] "abs #1 = (#1::real)";
 by (Simp_tac 1);
 qed "abs_one";
 
-Goalw [abs_real_def] "abs (-#1) = (#1::real)";
+Goalw [real_abs_def] "abs (-#1) = (#1::real)";
 by (Simp_tac 1);
 qed "abs_minus_one";
 Addsimps [abs_minus_one];
 
-Goalw [abs_real_def] "abs x =x | abs x = -(x::real)";
+Goalw [real_abs_def] "abs x =x | abs x = -(x::real)";
 by Auto_tac;
 qed "abs_disj";
 
-Goalw [abs_real_def] "(abs x < r) = (-r<x & x<(r::real))";
+Goalw [real_abs_def] "(abs x < r) = (-r<x & x<(r::real))";
 by Auto_tac;
 qed "abs_interval_iff";
 
-Goalw [abs_real_def] "(abs x <= r) = (-r<=x & x<=(r::real))";
+Goalw [real_abs_def] "(abs x <= r) = (-r<=x & x<=(r::real))";
 by Auto_tac;
 qed "abs_le_interval_iff";
 
-Goalw [abs_real_def] "(abs (x + (-y)) < r) = (y + (-r) < x & x < y + (r::real))";
-by Auto_tac;
-qed "abs_add_minus_interval_iff";
-
-Goalw [abs_real_def] "(#0::real) < k ==> #0 < k + abs(x)";
+Goalw [real_abs_def] "(#0::real) < k ==> #0 < k + abs(x)";
 by Auto_tac;
 qed "abs_add_pos_gt_zero";
 
-Goalw [abs_real_def] "(#0::real) < #1 + abs(x)";
+Goalw [real_abs_def] "(#0::real) < #1 + abs(x)";
 by Auto_tac;
 qed "abs_add_one_gt_zero";
 Addsimps [abs_add_one_gt_zero];
 
 (* 05/2000 *)
-Goalw [abs_real_def] "~ abs x < (#0::real)";
+Goalw [real_abs_def] "~ abs x < (#0::real)";
 by Auto_tac;
 qed "abs_not_less_zero";
 Addsimps [abs_not_less_zero];
@@ -226,44 +223,44 @@
     simpset()));
 qed "abs_circle";
 
-Goalw [abs_real_def] "(abs x <= (#0::real)) = (x = #0)";
+Goalw [real_abs_def] "(abs x <= (#0::real)) = (x = #0)";
 by Auto_tac;
 qed "abs_le_zero_iff";
 Addsimps [abs_le_zero_iff];
 
 Goal "((#0::real) < abs x) = (x ~= 0)";
-by (simp_tac (simpset() addsimps [abs_real_def]) 1);
+by (simp_tac (simpset() addsimps [real_abs_def]) 1);
 by (arith_tac 1);
 qed "real_0_less_abs_iff";
 Addsimps [real_0_less_abs_iff];
 
 Goal "abs (real_of_nat x) = real_of_nat x";
-by (auto_tac (claset() addIs [abs_eqI1],simpset()
-    addsimps [rename_numerals real_of_nat_ge_zero]));
+by (auto_tac (claset() addIs [abs_eqI1],
+              simpset() addsimps [rename_numerals real_of_nat_ge_zero]));
 qed "abs_real_of_nat_cancel";
 Addsimps [abs_real_of_nat_cancel];
 
 Goal "~ abs(x) + (#1::real) < x";
 by (rtac real_leD 1);
-by (auto_tac (claset() addIs [abs_ge_self RS real_le_trans],simpset()));
+by (auto_tac (claset() addIs [abs_ge_self RS real_le_trans], simpset()));
 qed "abs_add_one_not_less_self";
 Addsimps [abs_add_one_not_less_self];
-
+ 
 (* used in vector theory *)
 Goal "abs(w + x + (y::real)) <= abs(w) + abs(x) + abs(y)";
-by (auto_tac (claset() addSIs [(abs_triangle_ineq 
-    RS real_le_trans),real_add_left_le_mono1],
-    simpset() addsimps [real_add_assoc]));
+by (auto_tac (claset() addSIs [abs_triangle_ineq RS real_le_trans,
+                               real_add_left_le_mono1],
+              simpset() addsimps [real_add_assoc]));
 qed "abs_triangle_ineq_three";
 
-Goalw [abs_real_def] "abs(x - y) < y ==> (#0::real) < y";
+Goalw [real_abs_def] "abs(x - y) < y ==> (#0::real) < y";
 by (case_tac "#0 <= x - y" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "abs_diff_less_imp_gt_zero";
 
-Goalw [abs_real_def] "abs(x - y) < x ==> (#0::real) < x";
+Goalw [real_abs_def] "abs(x - y) < x ==> (#0::real) < x";
 by (case_tac "#0 <= x - y" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "abs_diff_less_imp_gt_zero2";
 
 Goal "abs(x - y) < y ==> (#0::real) < x";
@@ -274,8 +271,8 @@
 by (auto_tac (claset(),simpset() addsimps [abs_interval_iff]));
 qed "abs_diff_less_imp_gt_zero4";
 
-Goalw [abs_real_def] 
-     " abs(x) <= abs(x + (-y)) + abs((y::real))";
+Goalw [real_abs_def] 
+     "abs(x) <= abs(x + (-y)) + abs((y::real))";
 by Auto_tac;
 qed "abs_triangle_ineq_minus_cancel";
 
diff -r 07f75bf77a33 -r c838477b5c18 src/HOL/Real/RealAbs.thy
--- a/src/HOL/Real/RealAbs.thy	Thu Dec 21 10:16:07 2000 +0100
+++ b/src/HOL/Real/RealAbs.thy	Thu Dec 21 10:16:33 2000 +0100
@@ -9,6 +9,6 @@
 
 
 defs
-  abs_real_def "abs r == (if (#0::real) <= r then r else -r)"
+  real_abs_def "abs r == (if (#0::real) <= r then r else -r)"
 
 end
diff -r 07f75bf77a33 -r c838477b5c18 src/HOL/Real/RealPow.ML
--- a/src/HOL/Real/RealPow.ML	Thu Dec 21 10:16:07 2000 +0100
+++ b/src/HOL/Real/RealPow.ML	Thu Dec 21 10:16:33 2000 +0100
@@ -94,15 +94,13 @@
 Addsimps [realpow_eq_one];
 
 Goal "abs(-(#1 ^ n)) = (#1::real)";
-by (simp_tac (simpset() addsimps 
-    [abs_minus_cancel,abs_one]) 1);
+by (simp_tac (simpset() addsimps [abs_one]) 1);
 qed "abs_minus_realpow_one";
 Addsimps [abs_minus_realpow_one];
 
 Goal "abs((#-1) ^ n) = (#1::real)";
 by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps [abs_mult,
-         abs_minus_cancel,abs_one]));
+by (auto_tac (claset(),simpset() addsimps [abs_mult,abs_one]));
 qed "abs_realpow_minus_one";
 Addsimps [abs_realpow_minus_one];