# HG changeset patch
# User wenzelm
# Date 1008254703 -3600
# Node ID 0ed8bdd883e0792283a4a93029d7b5b734fca023
# Parent  3df60299a6d0bd61c98ec4ca6e993693f6855373
isatool expandshort;

diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/Algebra/poly/Degree.ML
--- a/src/HOL/Algebra/poly/Degree.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/Algebra/poly/Degree.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -152,7 +152,7 @@
 Goal "deg (monom m::'a::domain up) = m";
 by (rtac le_anti_sym 1);
 (* <= *)
-br deg_monom_ring 1;
+by (rtac deg_monom_ring 1);
 (* >= *)
 by (asm_simp_tac 
   (simpset() addsimps [deg_belowI, less_not_refl2 RS not_sym]) 1);
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/Hoare/Examples.ML
--- a/src/HOL/Hoare/Examples.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/Hoare/Examples.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -54,11 +54,11 @@
 \ DO IF a<b THEN (b := b-a; x := x+y) ELSE (a := a-b; y := y+x) FI OD \
 \ {a = gcd A B & 2*A*B = a*(x+y)}";
 by (hoare_tac (K all_tac) 1);
-by(Asm_simp_tac 1);
-by(asm_simp_tac (simpset() addsimps
+by (Asm_simp_tac 1);
+by (asm_simp_tac (simpset() addsimps
     (distribs @ [gcd_diff_r,not_less_iff_le, gcd_diff_l])) 1);
-by(arith_tac 1);
-by(asm_full_simp_tac (simpset() addsimps (distribs @ [gcd_nnn])) 1);
+by (arith_tac 1);
+by (asm_full_simp_tac (simpset() addsimps (distribs @ [gcd_nnn])) 1);
 qed "gcd_scm";
 
 (** Power by iterated squaring and multiplication **)
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/Hyperreal/EvenOdd.ML
--- a/src/HOL/Hyperreal/EvenOdd.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/Hyperreal/EvenOdd.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -113,7 +113,7 @@
 Addsimps [div_add_self_two_is_m];
 
 Goal "((m + m) + 2) div 2 = Suc m";
-by (rtac (div_add_self2 RS ssubst) 1);
+by (stac div_add_self2 1);
 by (Auto_tac);
 qed "div_add_self_two";
 
@@ -187,7 +187,7 @@
 Addsimps [mod_two_Suc_2m];
 
 Goal "(Suc (Suc (2 * m)) div 2) = Suc m";
-by (rtac (div_if RS ssubst) 1 THEN Auto_tac);
+by (stac div_if 1 THEN Auto_tac);
 qed "div_two_Suc_Suc_2m";
 Addsimps [div_two_Suc_Suc_2m];
 
@@ -239,14 +239,14 @@
 
 Goal "even n ==> (n + 1) div 2 = n div 2";
 by (rtac (CLAIM "2 * x = 2 * y ==> x = (y::nat)") 1);
-by (rtac (lemma_even_div RS ssubst) 1);
+by (stac lemma_even_div 1);
 by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex]));
 qed "lemma_even_div2";
 Addsimps [lemma_even_div2];
 
 Goal "~even n ==> (n + 1) div 2 = Suc (n div 2)";
 by (rtac (CLAIM "2 * x = 2 * y ==> x = (y::nat)") 1);
-by (rtac (lemma_not_even_div RS ssubst) 1);
+by (stac lemma_not_even_div 1);
 by (auto_tac (claset(),simpset() addsimps [even_not_odd,
     odd_Suc_mult_two_ex])); 
 by (cut_inst_tac [("m","Suc(2*m)"),("n","2")] mod_div_equality 1); 
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/Hyperreal/ExtraThms2.ML
--- a/src/HOL/Hyperreal/ExtraThms2.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/Hyperreal/ExtraThms2.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -220,7 +220,7 @@
 
 Goal "(real (n::nat) <= 0) = (n = 0)";
 by (rtac ((real_of_nat_zero) RS subst) 1);
-by (rtac (real_of_nat_le_iff RS ssubst) 1);
+by (stac real_of_nat_le_iff 1);
 by Auto_tac;
 qed "real_of_nat_le_zero_cancel_iff";
 Addsimps [real_of_nat_le_zero_cancel_iff];
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/Hyperreal/Lim.ML
--- a/src/HOL/Hyperreal/Lim.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/Hyperreal/Lim.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -1315,7 +1315,7 @@
 Goalw [nsderiv_def]
      "x \\<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ Suc (Suc 0)))";
 by (rtac ballI 1 THEN Asm_full_simp_tac 1 THEN Step_tac 1);
-by (forward_tac [Infinitesimal_add_not_zero] 1);
+by (ftac 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, realpow_two] 
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/Hyperreal/MacLaurin.ML
--- a/src/HOL/Hyperreal/MacLaurin.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/Hyperreal/MacLaurin.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -63,8 +63,8 @@
 by (asm_simp_tac (HOL_ss addsimps 
     [CLAIM "(a::real) * (b * (c * d)) = (d * a) * (b * c)"]
      delsimps [realpow_Suc]) 2);
-by (rtac (real_mult_inv_left RS ssubst) 2);
-by (rtac (real_mult_inv_left RS ssubst) 3);
+by (stac real_mult_inv_left 2);
+by (stac real_mult_inv_left 3);
 by (dtac (realpow_gt_zero RS real_not_refl2 RS not_sym) 2);
 by (assume_tac 2);
 by (rtac real_of_nat_fact_not_zero 2);
@@ -124,8 +124,8 @@
 by (rtac DERIV_cmult 2);
 by (rtac lemma_DERIV_subst 2);
 by DERIV_tac;
-by (rtac (fact_Suc RS ssubst) 2);
-by (rtac (real_of_nat_mult RS ssubst) 2);
+by (stac fact_Suc 2);
+by (stac real_of_nat_mult 2);
 by (simp_tac (simpset() addsimps [real_inverse_distrib] @
     real_mult_ac) 2);
 by (subgoal_tac "ALL ma. ma < n --> \
@@ -267,7 +267,7 @@
                  ("h","-h"),("n","n")] Maclaurin_objl 1);
 by (Asm_full_simp_tac 1);
 by (etac impE 1 THEN Step_tac 1);
-by (rtac (real_minus_mult_eq2 RS ssubst) 1);
+by (stac real_minus_mult_eq2 1);
 by (rtac DERIV_cmult 1);
 by (rtac lemma_DERIV_subst 1);
 by (rtac (read_instantiate [("g","uminus")] DERIV_chain2) 1);
@@ -463,7 +463,7 @@
 \                     else -cos(x)")] Maclaurin_all_le_objl 1);
 by (Step_tac 1);
 by (Asm_full_simp_tac 1);
-by (rtac (mod_Suc_eq_Suc_mod RS ssubst) 1);
+by (stac mod_Suc_eq_Suc_mod 1);
 by (cut_inst_tac [("m1","m")] (CLAIM "0 < (4::nat)" RS mod_less_divisor
     RS lemma_exhaust_less_4) 1);
 by (Step_tac 1);
@@ -479,7 +479,7 @@
 by (rtac sumr_fun_eq 1);
 by (Step_tac 1);
 by (rtac (CLAIM "x = y ==> x * z = y * (z::real)") 1);
-by (rtac (even_even_mod_4_iff RS ssubst) 1);
+by (stac even_even_mod_4_iff 1);
 by (cut_inst_tac [("m1","r")] (CLAIM "0 < (4::nat)" RS mod_less_divisor
     RS lemma_exhaust_less_4) 1);
 by (Step_tac 1);
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/Hyperreal/NSA.ML
--- a/src/HOL/Hyperreal/NSA.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/Hyperreal/NSA.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -144,7 +144,7 @@
 \         (EX Y. ALL X: {w. hypreal_of_real w : P}. X < Y)";
 by (rtac conjI 1);
 by (fast_tac (claset() addSDs [SReal_iff RS iffD1]) 1);
-by (Auto_tac THEN forward_tac [subsetD] 1 THEN assume_tac 1);
+by (Auto_tac THEN ftac subsetD 1 THEN assume_tac 1);
 by (dtac (SReal_iff RS iffD1) 1);
 by (Auto_tac THEN res_inst_tac [("x","ya")] exI 1);
 by Auto_tac;
@@ -201,7 +201,7 @@
 
 Goal "[| P <= Reals;  EX x. x: P;  EX Y. isUb Reals P Y |] \
 \     ==> EX t::hypreal. isLub Reals P t";
-by (forward_tac [SReal_hypreal_of_real_image] 1);
+by (ftac SReal_hypreal_of_real_image 1);
 by (Auto_tac THEN dtac lemma_isUb_hypreal_of_real 1);
 by (auto_tac (claset() addSIs [reals_complete, lemma_isLub_hypreal_of_real2], 
      simpset() addsimps [hypreal_of_real_isLub_iff,hypreal_of_real_isUb_iff]));
@@ -327,7 +327,7 @@
 Goal "[| x : Infinitesimal; y : HFinite |] ==> (x * y) : Infinitesimal";
 by (auto_tac (claset() addSDs [HFiniteD],
               simpset() addsimps [Infinitesimal_def]));
-by (forward_tac [hrabs_less_gt_zero] 1);
+by (ftac hrabs_less_gt_zero 1);
 by (dres_inst_tac [("x","r/t")] bspec 1); 
 by (blast_tac (claset() addIs [SReal_divide]) 1);
 by (asm_full_simp_tac (simpset() addsimps [hypreal_0_less_divide_iff]) 1); 
@@ -347,7 +347,7 @@
      "x: HInfinite ==> inverse x: Infinitesimal";
 by Auto_tac;
 by (eres_inst_tac [("x","inverse r")] ballE 1);
-by (rtac (hrabs_inverse RS ssubst) 1);
+by (stac hrabs_inverse 1);
 by (forw_inst_tac [("x1","r"),("z","abs x")] 
     (hypreal_inverse_gt_0 RS order_less_trans) 1);
 by (assume_tac 1);
@@ -600,8 +600,8 @@
 
 val prem1::prem2::rest = 
 goalw thy [approx_def] "[| a @= b; c @= d |] ==> a+c @= b+d";
-by (rtac (hypreal_minus_add_distrib RS ssubst) 1);
-by (rtac (hypreal_add_assoc RS ssubst) 1);
+by (stac hypreal_minus_add_distrib 1);
+by (stac hypreal_add_assoc 1);
 by (res_inst_tac [("y1","c")] (hypreal_add_left_commute RS subst) 1);
 by (rtac (hypreal_add_assoc RS subst) 1);
 by (rtac ([prem1,prem2] MRS Infinitesimal_add) 1);
@@ -919,7 +919,7 @@
 
 Goal "[|x: Reals; y: Reals|] ==> (x @= y) = (x = y)"; 
 by Auto_tac;
-by (rewrite_goals_tac [approx_def]);
+by (rewtac approx_def);
 by (dres_inst_tac [("x","y")] SReal_minus 1);
 by (dtac SReal_add 1 THEN assume_tac 1);
 by (dtac SReal_Infinitesimal_zero 1 THEN assume_tac 1);
@@ -984,7 +984,7 @@
  ------------------------------------------------------------------*)
 (* lemma about lubs *)
 Goal "!!(x::hypreal). [| isLub R S x; isLub R S y |] ==> x = y";
-by (forward_tac [isLub_isUb] 1);
+by (ftac isLub_isUb 1);
 by (forw_inst_tac [("x","y")] isLub_isUb 1);
 by (blast_tac (claset() addSIs [hypreal_le_anti_sym]
                 addSDs [isLub_le_isUb]) 1);
@@ -1022,7 +1022,7 @@
 
 Goal "[| x: HFinite;  isLub Reals {s. s: Reals & s < x} t; \
 \        r: Reals;  0 < r |] ==> x <= t + r";
-by (forward_tac [isLubD1a] 1);
+by (ftac isLubD1a 1);
 by (rtac ccontr 1 THEN dtac (linorder_not_le RS iffD2) 1);
 by (dres_inst_tac [("x","t")] SReal_add 1 THEN assume_tac 1);
 by (dres_inst_tac [("y","t + r")] (isLubD1 RS setleD) 1);
@@ -1055,7 +1055,7 @@
 \        isLub Reals {s. s: Reals & s < x} t; \
 \        r: Reals; 0 < r |] \
 \     ==> t + -r <= x";
-by (forward_tac [isLubD1a] 1);
+by (ftac isLubD1a 1);
 by (rtac ccontr 1 THEN dtac not_hypreal_leE 1);
 by (dtac SReal_minus 1 THEN dres_inst_tac [("x","t")] 
     SReal_add 1 THEN assume_tac 1);
@@ -1095,7 +1095,7 @@
 
 Goal "(x::hypreal): Reals ==> isLub Reals {s. s: Reals & s < x} x";
 by (auto_tac (claset() addSIs [isLubI2,lemma_SReal_ub,setgeI], simpset()));
-by (forward_tac [isUbD2a] 1);
+by (ftac isUbD2a 1);
 by (res_inst_tac [("x","x"),("y","y")] hypreal_linear_less2 1);
 by (auto_tac (claset() addSIs [order_less_imp_le], simpset()));
 by (EVERY1[dtac SReal_dense, assume_tac, assume_tac, Step_tac]);
@@ -1120,7 +1120,7 @@
 \        r: Reals; 0 < r |] \
 \     ==> -(x + -t) ~= r";
 by (auto_tac (claset(), simpset() addsimps [hypreal_minus_add_distrib]));
-by (forward_tac [isLubD1a] 1);
+by (ftac isLubD1a 1);
 by (dtac SReal_add_cancel 1 THEN assume_tac 1);
 by (dres_inst_tac [("x","-x")] SReal_minus 1);
 by (Asm_full_simp_tac 1);
@@ -1133,8 +1133,8 @@
 \        isLub Reals {s. s: Reals & s < x} t; \
 \        r: Reals; 0 < r |] \
 \     ==> abs (x + -t) < r";
-by (forward_tac [lemma_st_part1a] 1);
-by (forward_tac [lemma_st_part2a] 4);
+by (ftac lemma_st_part1a 1);
+by (ftac lemma_st_part2a 4);
 by Auto_tac;
 by (REPEAT(dtac order_le_imp_less_or_eq 1));
 by (auto_tac (claset() addDs [lemma_st_part_not_eq1,
@@ -1152,8 +1152,8 @@
  ----------------------------------------------*)
 Goal "x: HFinite ==> \
 \     EX t: Reals. ALL r: Reals. 0 < r --> abs (x + -t) < r";
-by (forward_tac [lemma_st_part_lub] 1 THEN Step_tac 1);
-by (forward_tac [isLubD1a] 1);
+by (ftac lemma_st_part_lub 1 THEN Step_tac 1);
+by (ftac isLubD1a 1);
 by (blast_tac (claset() addDs [lemma_st_part_major2]) 1);
 qed "lemma_st_part_Ex";
 
@@ -1242,9 +1242,9 @@
 
 Goal "[| x @= y; y :  HFinite - Infinitesimal |] \
 \     ==> inverse x @= inverse y";
-by (forward_tac [HFinite_diff_Infinitesimal_approx] 1);
+by (ftac HFinite_diff_Infinitesimal_approx 1);
 by (assume_tac 1);
-by (forward_tac [not_Infinitesimal_not_zero2] 1);
+by (ftac not_Infinitesimal_not_zero2 1);
 by (forw_inst_tac [("x","x")] not_Infinitesimal_not_zero2 1);
 by (REPEAT(dtac HFinite_inverse2 1));
 by (dtac approx_mult2 1 THEN assume_tac 1);
@@ -1282,8 +1282,8 @@
 
 Goal "(x : Infinitesimal) = (x*x : Infinitesimal)";
 by (auto_tac (claset() addIs [Infinitesimal_mult], simpset()));
-by (rtac ccontr 1 THEN forward_tac [Infinitesimal_inverse_HFinite] 1);
-by (forward_tac [not_Infinitesimal_not_zero] 1);
+by (rtac ccontr 1 THEN ftac Infinitesimal_inverse_HFinite 1);
+by (ftac not_Infinitesimal_not_zero 1);
 by (auto_tac (claset() addDs [Infinitesimal_HFinite_mult],
     simpset() addsimps [hypreal_mult_assoc]));
 qed "Infinitesimal_square_iff";
@@ -1431,14 +1431,14 @@
 qed "lemma_approx_less_zero";
 
 Goal "[| x @= y; x < 0; x ~: Infinitesimal |] ==> abs x @= abs y";
-by (forward_tac [lemma_approx_less_zero] 1);
+by (ftac lemma_approx_less_zero 1);
 by (REPEAT(assume_tac 1));
 by (REPEAT(dtac hrabs_minus_eqI2 1));
 by Auto_tac;
 qed "approx_hrabs1";
 
 Goal "[| x @= y; 0 < x; x ~: Infinitesimal |] ==> abs x @= abs y";
-by (forward_tac [lemma_approx_gt_zero] 1);
+by (ftac lemma_approx_gt_zero 1);
 by (REPEAT(assume_tac 1));
 by (REPEAT(dtac hrabs_eqI2 1));
 by Auto_tac;
@@ -1646,13 +1646,13 @@
  ------------------------------------------------------------------*)
 
 Goalw [st_def] "x: HFinite ==> st x @= x";
-by (forward_tac [st_part_Ex] 1 THEN Step_tac 1);
+by (ftac st_part_Ex 1 THEN Step_tac 1);
 by (rtac someI2 1);
 by (auto_tac (claset() addIs [approx_sym], simpset()));
 qed "st_approx_self";
 
 Goalw [st_def] "x: HFinite ==> st x: Reals";
-by (forward_tac [st_part_Ex] 1 THEN Step_tac 1);
+by (ftac st_part_Ex 1 THEN Step_tac 1);
 by (rtac someI2 1);
 by (auto_tac (claset() addIs [approx_sym], simpset()));
 qed "st_SReal";
@@ -1678,7 +1678,7 @@
 qed "st_eq_approx";
 
 Goal "[| x: HFinite; y: HFinite; x @= y |] ==> st x = st y";
-by (EVERY1 [forward_tac [st_approx_self],
+by (EVERY1 [ftac st_approx_self ,
     forw_inst_tac [("x","y")] st_approx_self,
     dtac st_SReal,dtac st_SReal]);
 by (fast_tac (claset() addEs [approx_trans,
@@ -1716,7 +1716,7 @@
 qed "HFinite_st_Infinitesimal_add";
 
 Goal "[| x: HFinite; y: HFinite |] ==> st (x + y) = st(x) + st(y)";
-by (forward_tac [HFinite_st_Infinitesimal_add] 1);
+by (ftac HFinite_st_Infinitesimal_add 1);
 by (forw_inst_tac [("x","y")] HFinite_st_Infinitesimal_add 1);
 by (Step_tac 1);
 by (subgoal_tac "st (x + y) = st ((st x + e) + (st y + ea))" 1);
@@ -1768,7 +1768,7 @@
 
 Goal "[| x: HFinite; y: HFinite |] \
 \              ==> st (x * y) = st(x) * st(y)";
-by (forward_tac [HFinite_st_Infinitesimal_add] 1);
+by (ftac HFinite_st_Infinitesimal_add 1);
 by (forw_inst_tac [("x","y")] HFinite_st_Infinitesimal_add 1);
 by (Step_tac 1);
 by (subgoal_tac "st (x * y) = st ((st x + e) * (st y + ea))" 1);
@@ -1841,9 +1841,9 @@
 qed "Infinitesimal_add_st_le_cancel";
 
 Goal "[| x: HFinite; y: HFinite; x <= y |] ==> st(x) <= st(y)";
-by (forward_tac [HFinite_st_Infinitesimal_add] 1);
+by (ftac HFinite_st_Infinitesimal_add 1);
 by (rotate_tac 1 1);
-by (forward_tac [HFinite_st_Infinitesimal_add] 1);
+by (ftac HFinite_st_Infinitesimal_add 1);
 by (Step_tac 1);
 by (rtac Infinitesimal_add_st_le_cancel 1);
 by (res_inst_tac [("x","ea"),("y","e")] 
@@ -2303,7 +2303,7 @@
 
 Goal "ALL n. abs(X n + -x) < inverse(real(Suc n)) \ 
 \     ==> Abs_hypreal(hyprel``{X}) @= hypreal_of_real x";
-by (rtac (approx_minus_iff RS ssubst) 1);
+by (stac approx_minus_iff 1);
 by (rtac (mem_infmal_iff RS subst) 1);
 by (etac real_seq_to_hypreal_Infinitesimal 1);
 qed "real_seq_to_hypreal_approx";
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/Hyperreal/NatStar.ML
--- a/src/HOL/Hyperreal/NatStar.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/Hyperreal/NatStar.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -189,7 +189,7 @@
 
 Goalw [congruent_def] 
       "congruent hypnatrel (%X. hypnatrel``{%n. f (X n)})";
-by (safe_tac (claset()));
+by Safe_tac;
 by (ALLGOALS(Fuf_tac));
 qed "starfunNat_congruent";
 
@@ -414,7 +414,7 @@
  ---------------------------------------------------------*)
 Goalw [congruent_def] 
       "congruent hypnatrel (%X. hypnatrel``{%n. f n (X n)})";
-by (safe_tac (claset()));
+by Safe_tac;
 by (ALLGOALS(Fuf_tac));
 qed "starfunNat_n_congruent";
 
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/Hyperreal/NthRoot.ML
--- a/src/HOL/Hyperreal/NthRoot.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/Hyperreal/NthRoot.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -70,7 +70,7 @@
 Goal "[| isLub (UNIV::real set) {x. x ^ n <= a & (0::real) < x} u; \
 \        0 < a; 0 < n |] ==> ALL k. a <= (u + inverse(real_of_posnat k)) ^ n";
 by (Step_tac 1);
-by (forward_tac [lemma_nth_realpow_seq] 1 THEN Step_tac 1);
+by (ftac lemma_nth_realpow_seq 1 THEN Step_tac 1);
 by (auto_tac (claset() addEs [real_less_asym],
     simpset() addsimps [real_le_def]));
 by (fold_tac [real_le_def]);
@@ -85,7 +85,7 @@
 Goal "[| (0::real) < a; 0 < n; \
 \    isLub (UNIV::real set) \
 \    {x. x ^ n <= a & 0 < x} u |] ==> a <= u ^ n";
-by (forward_tac [lemma_nth_realpow_isLub_ge] 1 THEN Step_tac 1);
+by (ftac lemma_nth_realpow_isLub_ge 1 THEN Step_tac 1);
 by (rtac (LIMSEQ_inverse_real_of_posnat_add RS LIMSEQ_pow 
     RS LIMSEQ_le_const) 1);
 by (auto_tac (claset(),simpset() addsimps [real_of_nat_def,
@@ -133,7 +133,7 @@
 Goal "[| (0::real) < a; 0 < n; \
 \    isLub (UNIV::real set) \
 \    {x. x ^ n <= a & 0 < x} u |] ==> u ^ n <= a";
-by (forward_tac [lemma_nth_realpow_isLub_le] 1 THEN Step_tac 1);
+by (ftac lemma_nth_realpow_isLub_le 1 THEN Step_tac 1);
 by (rtac (LIMSEQ_inverse_real_of_posnat_add_minus_mult RS LIMSEQ_pow 
     RS LIMSEQ_le_const2) 1);
 by (auto_tac (claset(),simpset() addsimps [real_of_nat_def,real_of_posnat_Suc]));
@@ -141,14 +141,14 @@
 
 (*----------- The theorem at last! -----------*)
 Goal "[| (0::real) < a; 0 < n |] ==> EX r. r ^ n = a";
-by (forward_tac [nth_realpow_isLub_ex] 1 THEN Auto_tac);
+by (ftac nth_realpow_isLub_ex 1 THEN Auto_tac);
 by (auto_tac (claset() addIs [realpow_nth_le,
     realpow_nth_ge,real_le_anti_sym],simpset()));
 qed "realpow_nth";
 
 (* positive only *)
 Goal "[| (0::real) < a; 0 < n |] ==> EX r. 0 < r & r ^ n = a";
-by (forward_tac [nth_realpow_isLub_ex] 1 THEN Auto_tac);
+by (ftac nth_realpow_isLub_ex 1 THEN Auto_tac);
 by (auto_tac (claset() addIs [realpow_nth_le,
     realpow_nth_ge,real_le_anti_sym,
     lemma_nth_realpow_isLub_gt_zero],simpset()));
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/Hyperreal/SEQ.ML
--- a/src/HOL/Hyperreal/SEQ.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/Hyperreal/SEQ.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -671,7 +671,7 @@
 Goalw [convergent_def] 
      "[| Bseq X; ALL m n. m <= n --> X m <= X n |] \
 \                ==> convergent X";
-by (forward_tac [Bseq_isLub] 1);
+by (ftac Bseq_isLub 1);
 by (Step_tac 1);
 by (case_tac "EX m. X m = U" 1 THEN Auto_tac);
 by (blast_tac (claset() addDs [lemma_converg1,
@@ -679,7 +679,7 @@
 (* second case *)
 by (res_inst_tac [("x","U")] exI 1);
 by (stac LIMSEQ_iff 1 THEN Step_tac 1);
-by (forward_tac [lemma_converg2] 1 THEN assume_tac 1);
+by (ftac lemma_converg2 1 THEN assume_tac 1);
 by (dtac lemma_converg4 1 THEN Auto_tac);
 by (res_inst_tac [("x","m")] exI 1 THEN Step_tac 1);
 by (subgoal_tac "X m <= X n" 1 THEN Fast_tac 2);
@@ -711,7 +711,7 @@
  -------------------------------*)
 Goalw [monoseq_def] "[| Bseq X; monoseq X |] ==> convergent X";
 by (Step_tac 1);
-by (rtac (convergent_minus_iff RS ssubst) 2);
+by (stac convergent_minus_iff 2);
 by (dtac (Bseq_minus_iff RS ssubst) 2);
 by (auto_tac (claset() addSIs [Bseq_mono_convergent], simpset()));
 qed "Bseq_monoseq_convergent";
@@ -960,7 +960,7 @@
 Goalw [NSconvergent_def,NSLIMSEQ_def]
       "NSCauchy X = NSconvergent X";
 by (Step_tac 1);
-by (forward_tac [NSCauchy_NSBseq] 1);
+by (ftac NSCauchy_NSBseq 1);
 by (auto_tac (claset() addIs [approx_trans2], 
     simpset() addsimps 
     [NSBseq_def,NSCauchy_def]));
@@ -1124,8 +1124,8 @@
 by (dres_inst_tac [("x","inverse r")] spec 1 THEN Step_tac 1);
 by (res_inst_tac [("x","N")] exI 1 THEN Step_tac 1);
 by (dtac spec 1 THEN Auto_tac);
-by (forward_tac [real_inverse_gt_0] 1);
-by (forward_tac [order_less_trans] 1 THEN assume_tac 1);
+by (ftac real_inverse_gt_0 1);
+by (ftac order_less_trans 1 THEN assume_tac 1);
 by (forw_inst_tac [("x","f n")] real_inverse_gt_0 1);
 by (asm_simp_tac (simpset() addsimps [abs_eqI2]) 1);
 by (res_inst_tac [("t","r")] (real_inverse_inverse RS subst) 1);
@@ -1241,11 +1241,11 @@
      "[| 0 <= x; x < 1 |] ==> (%n. x ^ n) ----NS> 0";
 by (auto_tac (claset() addSDs [convergent_realpow],
               simpset() addsimps [convergent_NSconvergent_iff]));
-by (forward_tac [NSconvergentD] 1);
+by (ftac NSconvergentD 1);
 by (auto_tac (claset(),
         simpset() addsimps [NSLIMSEQ_def, NSCauchy_NSconvergent_iff RS sym,
                             NSCauchy_def, starfunNat_pow]));
-by (forward_tac [HNatInfinite_add_one] 1);
+by (ftac HNatInfinite_add_one 1);
 by (dtac bspec 1 THEN assume_tac 1);
 by (dtac bspec 1 THEN assume_tac 1);
 by (dres_inst_tac [("x","N + (1::hypnat)")] bspec 1 THEN assume_tac 1);
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/Hyperreal/Series.ML
--- a/src/HOL/Hyperreal/Series.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/Hyperreal/Series.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -283,7 +283,7 @@
      "(ALL m. n <= Suc m --> f(m) = 0) ==> f sums (sumr 0 n f)";
 by (Step_tac 1);
 by (res_inst_tac [("x","n")] exI 1);
-by (Step_tac 1 THEN forward_tac [le_imp_less_or_eq] 1);
+by (Step_tac 1 THEN ftac le_imp_less_or_eq 1);
 by (Step_tac 1);
 by (dres_inst_tac [("f","f")] sumr_split_add_minus 1);
 by (ALLGOALS (Asm_simp_tac));
@@ -297,7 +297,7 @@
      "(ALL m. n <= m --> f(m) = 0) ==> f sums (sumr 0 n f)";
 by (Step_tac 1);
 by (res_inst_tac [("x","n")] exI 1);
-by (Step_tac 1 THEN forward_tac [le_imp_less_or_eq] 1);
+by (Step_tac 1 THEN ftac le_imp_less_or_eq 1);
 by (Step_tac 1);
 by (dres_inst_tac [("f","f")] sumr_split_add_minus 1);
 by (ALLGOALS (Asm_simp_tac));
@@ -571,7 +571,7 @@
 
 Goal "[| c < 1; ALL n. N <= n --> abs(f(Suc n)) <= c*abs(f n) |] \
 \     ==> summable f";
-by (forward_tac [ratio_test_lemma2] 1);
+by (ftac ratio_test_lemma2 1);
 by Auto_tac;  
 by (res_inst_tac [("g","%n. (abs (f N)/(c ^ N))*c ^ n")] 
     summable_comparison_test 1);
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/Hyperreal/Star.ML
--- a/src/HOL/Hyperreal/Star.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/Hyperreal/Star.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -193,7 +193,7 @@
  -----------------------------------------------------------------------*) 
 
 Goalw [congruent_def] "congruent hyprel (%X. hyprel``{%n. f (X n)})";
-by (safe_tac (claset()));
+by Safe_tac;
 by (ALLGOALS(Fuf_tac));
 qed "starfun_congruent";
 
@@ -472,7 +472,7 @@
 Goal "(Abs_hypreal(hyprel``{X}) @= Abs_hypreal(hyprel``{Y})) = \
 \     (ALL m. {n. abs (X n + - Y n) < \
 \                 inverse(real(Suc m))} : FreeUltrafilterNat)";
-by (rtac (approx_minus_iff RS ssubst) 1);
+by (stac approx_minus_iff 1);
 by (rtac (mem_infmal_iff RS subst) 1);
 by (auto_tac (claset(), 
               simpset() addsimps [hypreal_minus, hypreal_add,
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/Hyperreal/Transcendental.ML
--- a/src/HOL/Hyperreal/Transcendental.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/Hyperreal/Transcendental.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -211,7 +211,7 @@
 Goal "sqrt(x ^ 2) = abs(x)";
 by (rtac (abs_realpow_two RS subst) 1);
 by (rtac (real_sqrt_abs_abs RS subst) 1);
-by (rtac (real_pow_sqrt_eq_sqrt_pow RS ssubst) 1);
+by (stac real_pow_sqrt_eq_sqrt_pow 1);
 by (auto_tac (claset(),simpset() addsimps [numeral_2_eq_2, abs_mult,abs_ge_zero]));
 qed "real_sqrt_abs";
 Addsimps [real_sqrt_abs];
@@ -228,12 +228,12 @@
 qed "real_sqrt_pow2_gt_zero";
 
 Goal "0 < x ==> sqrt x ~= 0";
-by (forward_tac [real_sqrt_pow2_gt_zero] 1);
+by (ftac real_sqrt_pow2_gt_zero 1);
 by (auto_tac (claset(),simpset() addsimps [numeral_2_eq_2, real_less_not_refl]));
 qed "real_sqrt_not_eq_zero";
 
 Goal "0 < x ==> inverse (sqrt(x)) ^ 2 = inverse x";
-by (forward_tac [real_sqrt_not_eq_zero] 1);
+by (ftac real_sqrt_not_eq_zero 1);
 by (cut_inst_tac [("n1","2"),("r1","sqrt x")] (realpow_inverse RS sym) 1);
 by (auto_tac (claset() addDs [real_sqrt_gt_zero_pow2],simpset()));
 qed "real_inv_sqrt_pow2";
@@ -286,8 +286,8 @@
     delsimps [fact_Suc]));
 by (rtac real_mult_le_le_mono2 1);
 by (res_inst_tac [("w1","abs x")] (real_mult_commute RS ssubst) 2);
-by (rtac (fact_Suc RS ssubst) 2);
-by (rtac (real_of_nat_mult RS ssubst) 2);
+by (stac fact_Suc 2);
+by (stac real_of_nat_mult 2);
 by (auto_tac (claset(),simpset() addsimps [abs_mult,real_inverse_distrib,
     abs_ge_zero]));
 by (auto_tac (claset(), simpset() addsimps 
@@ -402,7 +402,7 @@
 by (auto_tac (claset(),simpset() addsimps [sumr_mult] delsimps [sumr_Suc]));
 by (rtac sumr_subst 1);
 by (strip_tac 1);
-by (rtac (lemma_realpow_diff RS ssubst) 1);
+by (stac lemma_realpow_diff 1);
 by (auto_tac (claset(),simpset() addsimps real_mult_ac));
 qed "lemma_realpow_diff_sumr";
 
@@ -410,7 +410,7 @@
 \     (x - y) * sumr 0 (Suc n) (%p. (x ^ p) * (y ^(n - p)))";
 by (induct_tac "n" 1);
 by (auto_tac (claset(),simpset() delsimps [sumr_Suc]));
-by (rtac (sumr_Suc RS ssubst) 1);
+by (stac sumr_Suc 1);
 by (dtac sym 1);
 by (auto_tac (claset(),simpset() addsimps [lemma_realpow_diff_sumr,
     real_add_mult_distrib2,real_diff_def] @ 
@@ -424,7 +424,7 @@
     realpow_add RS sym] delsimps [sumr_Suc]));
 by (res_inst_tac [("c1","x - y")] (real_mult_left_cancel RS iffD1) 1);
 by (rtac (real_minus_minus RS subst) 2);
-by (rtac (real_minus_mult_eq1 RS ssubst) 2);
+by (stac real_minus_mult_eq1 2);
 by (auto_tac (claset(),simpset() addsimps [lemma_realpow_diff_sumr2 
     RS sym] delsimps [sumr_Suc]));
 qed "lemma_realpow_rev_sumr";
@@ -581,7 +581,7 @@
 Goal "[| h ~= 0; abs z <= K; abs (z + h) <= K |] \
 \     ==> abs (((z + h) ^ n - z ^ n) * inverse h - real n * z ^ (n - Suc 0)) \
 \         <= real n * real (n - Suc 0) * K ^ (n - 2) * abs h";
-by (rtac (lemma_termdiff2 RS ssubst) 1);
+by (stac lemma_termdiff2 1);
 by (asm_full_simp_tac (simpset() addsimps [abs_mult,real_mult_commute]) 2);
 by (stac real_mult_commute 2); 
 by (rtac (sumr_rabs RS real_le_trans) 2);
@@ -812,9 +812,9 @@
 Goalw [diffs_def]  
       "diffs (%n. inverse(real (fact n))) = (%n. inverse(real (fact n)))";
 by (rtac ext 1);
-by (rtac (fact_Suc RS ssubst) 1);
-by (rtac (real_of_nat_mult RS ssubst) 1);
-by (rtac (real_inverse_distrib RS ssubst) 1);
+by (stac fact_Suc 1);
+by (stac real_of_nat_mult 1);
+by (stac real_inverse_distrib 1);
 by (auto_tac (claset(),simpset() addsimps [real_mult_assoc RS sym]));
 qed "exp_fdiffs";
 
@@ -825,10 +825,10 @@
 \                (- 1) ^ (n div 2)/(real (fact n)) \
 \             else 0)";
 by (rtac ext 1);
-by (rtac (fact_Suc RS ssubst) 1);
-by (rtac (real_of_nat_mult RS ssubst) 1);
-by (rtac (even_Suc RS ssubst) 1);
-by (rtac (real_inverse_distrib RS ssubst) 1);
+by (stac fact_Suc 1);
+by (stac real_of_nat_mult 1);
+by (stac even_Suc 1);
+by (stac real_inverse_distrib 1);
 by Auto_tac;
 qed "sin_fdiffs";
 
@@ -838,10 +838,10 @@
 \      = (if even n then \
 \                (- 1) ^ (n div 2)/(real (fact n)) \
 \             else 0)";
-by (rtac (fact_Suc RS ssubst) 1);
-by (rtac (real_of_nat_mult RS ssubst) 1);
-by (rtac (even_Suc RS ssubst) 1);
-by (rtac (real_inverse_distrib RS ssubst) 1);
+by (stac fact_Suc 1);
+by (stac real_of_nat_mult 1);
+by (stac even_Suc 1);
+by (stac real_inverse_distrib 1);
 by Auto_tac;
 qed "sin_fdiffs2";
 
@@ -852,10 +852,10 @@
 \      = (%n. - (if even n then 0 \
 \          else (- 1) ^ ((n - Suc 0)div 2)/(real (fact n))))";
 by (rtac ext 1);
-by (rtac (fact_Suc RS ssubst) 1);
-by (rtac (real_of_nat_mult RS ssubst) 1);
-by (rtac (even_Suc RS ssubst) 1);
-by (rtac (real_inverse_distrib RS ssubst) 1);
+by (stac fact_Suc 1);
+by (stac real_of_nat_mult 1);
+by (stac even_Suc 1);
+by (stac real_inverse_distrib 1);
 by (res_inst_tac [("z1","real (Suc n)")] (real_mult_commute RS ssubst) 1);
 by (res_inst_tac [("z1","inverse(real (Suc n))")] 
      (real_mult_commute RS ssubst) 1);
@@ -869,10 +869,10 @@
 \                (- 1) ^ (n div 2)/(real (fact n)) else 0) n\
 \      = - (if even n then 0 \
 \          else (- 1) ^ ((n - Suc 0)div 2)/(real (fact n)))";
-by (rtac (fact_Suc RS ssubst) 1);
-by (rtac (real_of_nat_mult RS ssubst) 1);
-by (rtac (even_Suc RS ssubst) 1);
-by (rtac (real_inverse_distrib RS ssubst) 1);
+by (stac fact_Suc 1);
+by (stac real_of_nat_mult 1);
+by (stac even_Suc 1);
+by (stac real_inverse_distrib 1);
 by (res_inst_tac [("z1","real (Suc n)")] (real_mult_commute RS ssubst) 1);
 by (res_inst_tac [("z1","inverse (real (Suc n))")] 
      (real_mult_commute RS ssubst) 1);
@@ -895,7 +895,7 @@
 val lemma_exp_ext = result();
 
 Goalw [exp_def] "DERIV exp x :> exp(x)";
-by (rtac (lemma_exp_ext RS ssubst) 1);
+by (stac lemma_exp_ext 1);
 by (subgoal_tac "DERIV (%u. suminf (%n. inverse (real (fact n)) * u ^ n)) x \
 \    :> suminf (%n. diffs (%n. inverse (real (fact n))) n * x ^ n)" 1);
 by (res_inst_tac [("K","1 + abs(x)")] termdiffs 2);
@@ -918,7 +918,7 @@
 val lemma_cos_ext = result();
 
 Goalw [cos_def] "DERIV sin x :> cos(x)";
-by (rtac (lemma_sin_ext RS ssubst) 1);
+by (stac lemma_sin_ext 1);
 by (auto_tac (claset(),simpset() addsimps [sin_fdiffs2 RS sym]));
 by (res_inst_tac [("K","1 + abs(x)")] termdiffs 1);
 by (auto_tac (claset() addIs [sin_converges, cos_converges, sums_summable] 
@@ -929,7 +929,7 @@
 Addsimps [DERIV_sin];
 
 Goal "DERIV cos x :> -sin(x)";
-by (rtac (lemma_cos_ext RS ssubst) 1);
+by (stac lemma_cos_ext 1);
 by (auto_tac (claset(),simpset() addsimps [lemma_sin_minus,
     cos_fdiffs2 RS sym,real_minus_mult_eq1]));
 by (res_inst_tac [("K","1 + abs(x)")] termdiffs 1);
@@ -988,7 +988,7 @@
     [CLAIM_SIMP "(%x. exp(-x)) = exp o (%x. - x)" [ext]]));
 by (rtac (real_mult_1_right RS subst) 1);
 by (rtac (real_minus_mult_eq1 RS subst) 1);
-by (rtac (real_minus_mult_eq2 RS ssubst) 1);
+by (stac real_minus_mult_eq2 1);
 by (rtac DERIV_chain 1);
 by (rtac DERIV_minus 2);
 by Auto_tac;
@@ -1034,7 +1034,7 @@
 
 Goal "0 <= exp x";
 by (res_inst_tac [("t","x")] (real_sum_of_halves RS subst) 1);
-by (rtac (exp_add RS ssubst) 1 THEN Auto_tac);
+by (stac exp_add 1 THEN Auto_tac);
 qed "exp_ge_zero";
 Addsimps [exp_ge_zero];
 
@@ -1337,7 +1337,7 @@
 Addsimps [sin_cos_squared_add];
 
 Goal "(cos(x) ^ 2) + (sin(x) ^ 2) = 1";
-by (rtac (real_add_commute RS ssubst) 1);
+by (stac real_add_commute 1);
 by (simp_tac (simpset() delsimps [realpow_Suc]) 1);
 qed "sin_cos_squared_add2";
 Addsimps [sin_cos_squared_add2];
@@ -1586,14 +1586,14 @@
 by (stac (CLAIM "6 = 2 * (3::real)") 2);
 by (rtac real_mult_less_mono 2);  
 by (auto_tac (claset(),simpset() addsimps [real_of_nat_Suc] delsimps [fact_Suc]));
-by (rtac (fact_Suc RS ssubst) 1);
-by (rtac (fact_Suc RS ssubst) 1);
-by (rtac (fact_Suc RS ssubst) 1);
-by (rtac (fact_Suc RS ssubst) 1);
-by (rtac (real_of_nat_mult RS ssubst) 1);
-by (rtac (real_of_nat_mult RS ssubst) 1);
-by (rtac (real_of_nat_mult RS ssubst) 1);
-by (rtac (real_of_nat_mult RS ssubst) 1);
+by (stac fact_Suc 1);
+by (stac fact_Suc 1);
+by (stac fact_Suc 1);
+by (stac fact_Suc 1);
+by (stac real_of_nat_mult 1);
+by (stac real_of_nat_mult 1);
+by (stac real_of_nat_mult 1);
+by (stac real_of_nat_mult 1);
 by (simp_tac (simpset() addsimps [real_divide_def,
     real_inverse_distrib] delsimps [fact_Suc]) 1);
 by (auto_tac (claset(),simpset() addsimps [real_mult_assoc RS sym] 
@@ -1659,9 +1659,9 @@
 by (simp_tac (simpset() addsimps [real_mult_assoc RS sym] 
     delsimps [fact_Suc]) 1);
 by (rtac ((CLAIM "real(n::nat) * 4 = real(4 * n)") RS ssubst) 1);
-by (rtac (fact_Suc RS ssubst) 1);
-by (rtac (real_of_nat_mult RS ssubst) 1);
-by (rtac (real_of_nat_mult RS ssubst) 1);
+by (stac fact_Suc 1);
+by (stac real_of_nat_mult 1);
+by (stac real_of_nat_mult 1);
 by (rtac real_mult_less_mono 1);
 by (Force_tac 1);
 by (Force_tac 2);
@@ -1884,7 +1884,7 @@
 qed "cos_ge_zero";
 
 Goal "[| 0 < x; x < pi  |] ==> 0 < sin x";
-by (rtac (sin_cos_eq RS ssubst) 1);
+by (stac sin_cos_eq 1);
 by (rotate_tac 1 1);
 by (dtac (real_sum_of_halves RS ssubst) 1);
 by (auto_tac (claset() addSIs [cos_gt_zero_pi],
@@ -2425,7 +2425,7 @@
 
 Goal "cos (3 / 2 * pi) = 0";
 by (rtac (CLAIM "(1::real) + 1/2 = 3/2" RS subst) 1);
-by (rtac (real_add_mult_distrib RS ssubst) 1);
+by (stac real_add_mult_distrib 1);
 by (auto_tac (claset(),simpset() addsimps [cos_add] @ real_mult_ac));
 qed "cos_3over2_pi";
 Addsimps [cos_3over2_pi];
@@ -2437,7 +2437,7 @@
 
 Goal "sin (3 / 2 * pi) = - 1";
 by (rtac (CLAIM "(1::real) + 1/2 = 3/2" RS subst) 1);
-by (rtac (real_add_mult_distrib RS ssubst) 1);
+by (stac real_add_mult_distrib 1);
 by (auto_tac (claset(),simpset() addsimps [sin_add] @real_mult_ac));
 qed "sin_3over2_pi";
 Addsimps [sin_3over2_pi];
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/IMPP/Hoare.ML
--- a/src/HOL/IMPP/Hoare.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/IMPP/Hoare.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -408,20 +408,20 @@
 (*
 Goal "!Q. G |-{%Z s. ~(? s'. <c,s> -c-> s')}. c .{Q}";
 by (induct_tac "c" 1);
-auto();
-br conseq1 1;
-br hoare_derivs.Skip 1;
+by Auto_tac;
+by (rtac conseq1 1);
+by (rtac hoare_derivs.Skip 1);
 force 1;
-br conseq1 1;
-br hoare_derivs.Ass 1;
+by (rtac conseq1 1);
+by (rtac hoare_derivs.Ass 1);
 force 1;
 by (defer_tac 1);
 ###
-br hoare_derivs.Comp 1;
-bd spec 2;
-bd spec 2;
-ba 2;
-be conseq1 2;
+by (rtac hoare_derivs.Comp 1);
+by (dtac spec 2);
+by (dtac spec 2);
+by (assume_tac 2);
+by (etac conseq1 2);
 by (Clarsimp_tac 2);
 force 1;
 *)
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/Induct/Com.ML
--- a/src/HOL/Induct/Com.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/Induct/Com.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -37,7 +37,7 @@
 by (etac exec.induct 1);
 by (Blast_tac 3);
 by (Blast_tac 1);
-by (rewrite_goals_tac [single_valued_def]);
+by (rewtac single_valued_def);
 by (REPEAT (blast_tac (claset() addEs [exec_WHILE_case]) 1));
 qed "single_valued_exec";
 
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/Induct/SList.ML
--- a/src/HOL/Induct/SList.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/Induct/SList.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -448,8 +448,8 @@
 val [] = Goal "(Alls u:A. P u) = (!n. n < length A --> P(nth n A))";
 by (induct_thm_tac list_induct "A" 1);
 by (ALLGOALS Asm_simp_tac);
-br trans 1;
-br (nat_case_dist RS sym) 2;
+by (rtac trans 1);
+by (rtac (nat_case_dist RS sym) 2);
 by (ALLGOALS Asm_simp_tac);
 qed "alls_P_eq_P_nth";
 
@@ -501,10 +501,10 @@
 by (ALLGOALS Asm_simp_tac);
 by (res_inst_tac [("x","xa")] exI 1);
 by (ALLGOALS Asm_simp_tac);
-br impI 1;
+by (rtac impI 1);
 by (rotate_tac 1 1);
 by (ALLGOALS  Asm_full_simp_tac);
-be exE 1; be conjE 1;
+by (etac exE 1); by (etac conjE 1);
 by (res_inst_tac [("x","y")] exI 1);
 by (asm_simp_tac (HOL_ss addsimps [if_cancel]) 1);
 qed "mem_map_aux1";
@@ -513,14 +513,14 @@
 "(? y. y mem q & x = f y) --> x mem (map f q)";
 by (induct_thm_tac list_induct "q" 1);
 by (Asm_simp_tac 1);
-br impI 1;
-be exE 1;
-be conjE 1;
+by (rtac impI 1);
+by (etac exE 1);
+by (etac conjE 1);
 by (ALLGOALS Asm_simp_tac);
 by (case_tac "xa = y" 1);
 by (rotate_tac 2 1);
 by (asm_full_simp_tac (HOL_ss addsimps [if_cancel]) 1);
-be impE 1;
+by (etac impE 1);
 by (asm_simp_tac (HOL_ss addsimps [if_cancel]) 1);
 by (case_tac "f xa = f y" 2);
 by (res_inst_tac [("x","y")] exI 1);
@@ -531,9 +531,9 @@
 
 Goal
 "x mem (map f q) = (? y. y mem q & x = f y)";
-br iffI 1;
-br (mem_map_aux1 RS mp) 1;
-br (mem_map_aux2 RS mp) 2;
+by (rtac iffI 1);
+by (rtac (mem_map_aux1 RS mp) 1);
+by (rtac (mem_map_aux2 RS mp) 2);
 by (ALLGOALS atac);
 qed "mem_map";
 
@@ -685,7 +685,7 @@
 
 
 Goalw [o_def] "map(f o g) = ((map f) o (map g))";
-br ext 1;
+by (rtac ext 1);
 by (simp_tac (HOL_ss addsimps [map_compose RS sym,o_def]) 1);
 qed "map_compose_ext";
 
@@ -839,8 +839,8 @@
 
 Goal "ALL A. length(A) = n --> take(A@B) n = A";
 by (induct_tac "n" 1);
-br allI 1;
-br allI 2;
+by (rtac allI 1);
+by (rtac allI 2);
 by (induct_thm_tac list_induct "A" 1);
 by (induct_thm_tac list_induct "A" 3);
 by (ALLGOALS  Asm_full_simp_tac);
@@ -848,8 +848,8 @@
 
 Goal "ALL A. length(A) = n --> take(A@B) (n+k) = A@take B k";
 by (induct_tac "n" 1);
-br allI 1;
-br allI 2;
+by (rtac allI 1);
+by (rtac allI 2);
 by (induct_thm_tac list_induct "A" 1);
 by (induct_thm_tac list_induct "A" 3);
 by (ALLGOALS  Asm_full_simp_tac);
@@ -865,8 +865,8 @@
 
 Goal "ALL A. length(A) = n --> drop(A@B)n = B";
 by (induct_tac "n" 1);
-br allI 1;
-br allI 2;
+by (rtac allI 1);
+by (rtac allI 2);
 by (induct_thm_tac list_induct "A" 1);
 by (induct_thm_tac list_induct "A" 3);
 by (ALLGOALS  Asm_full_simp_tac);
@@ -874,8 +874,8 @@
 
 Goal "ALL A. length(A) = n --> drop(A@B)(n+k) = drop B k";
 by (induct_tac "n" 1);
-br allI 1;
-br allI 2;
+by (rtac allI 1);
+by (rtac allI 2);
 by (induct_thm_tac list_induct "A" 1);
 by (induct_thm_tac list_induct "A" 3);
 by (ALLGOALS  Asm_full_simp_tac);
@@ -884,8 +884,8 @@
 
 Goal "ALL A. length(A) = n --> drop A n = []";
 by (induct_tac "n" 1);
-br allI 1;
-br allI 2;
+by (rtac allI 1);
+by (rtac allI 2);
 by (induct_thm_tac list_induct "A" 1);
 by (induct_thm_tac list_induct "A" 3);
 by Auto_tac; 
@@ -902,8 +902,8 @@
 
 Goal "ALL A. length(A) = n --> take A n = A";
 by (induct_tac "n" 1);
-br allI 1;
-br allI 2;
+by (rtac allI 1);
+by (rtac allI 2);
 by (induct_thm_tac list_induct "A" 1);
 by (induct_thm_tac list_induct "A" 3);
 by (ALLGOALS (simp_tac (simpset())));
@@ -949,9 +949,9 @@
 "[| !a. f a e = a; !a. f e a = a;          \
 \   !a b c. f a (f b c) = f(f a b) c |]   \
 \ ==> foldl f e (A @ B) = f(foldl f e A)(foldl f e B)";
-br trans 1;
-br foldl_append 1;
-br (foldl_neutr_distr) 1;
+by (rtac trans 1);
+by (rtac foldl_append 1);
+by (rtac (foldl_neutr_distr) 1);
 by Auto_tac; 
 qed "foldl_append_sym";
 
@@ -983,7 +983,7 @@
 "[| !a. f e a = a; !a b c. f a (f b c) = f(f a b) c |] ==> \
 \ foldr f e (A @ B) = f (foldr f e A) (foldr f e B)";
 by Auto_tac;
-br foldr_neutr_distr 1;
+by (rtac foldr_neutr_distr 1);
 by Auto_tac; 
 qed "foldr_append2";
 
@@ -1020,7 +1020,7 @@
 Goal "ALL i. i < length(A)  --> nth i (map f A) = f(nth i A)";
 by (induct_thm_tac list_induct "A" 1);
 by (ALLGOALS(asm_simp_tac (simpset() delsimps [less_Suc_eq])));
-br allI 1;
+by (rtac allI 1);
 by (induct_tac "i" 1);
 by (ALLGOALS(asm_simp_tac (simpset() addsimps [nth_0,nth_Suc])));
 qed_spec_mp "nth_map";
@@ -1028,7 +1028,7 @@
 Goal "ALL i. i < length(A)  --> nth i(A@B) = nth i A";
 by (induct_thm_tac list_induct "A" 1);
 by (ALLGOALS(asm_simp_tac (simpset() delsimps [less_Suc_eq])));
-br allI 1;
+by (rtac allI 1);
 by (induct_tac "i" 1);
 by (ALLGOALS(asm_simp_tac (simpset() addsimps [nth_0,nth_Suc])));
 qed_spec_mp "nth_app_cancel_right";
@@ -1085,9 +1085,9 @@
 qed "foldl_rev";
 
 Goal "foldr f b (rev l) = foldl (%x y. f y x) b l";
-br sym 1;
-br trans 1;
-br foldl_rev 2;
+by (rtac sym 1);
+by (rtac trans 1);
+by (rtac foldl_rev 2);
 by (simp_tac (HOL_ss addsimps [rev_rev_ident]) 1);
 qed "foldr_rev";
 
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/Integ/Bin.ML
--- a/src/HOL/Integ/Bin.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/Integ/Bin.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -313,7 +313,7 @@
 Goalw [zabs_def]
  "abs(number_of x::int) = \
 \ (if number_of x < (0::int) then -number_of x else number_of x)";
-by(rtac refl 1);
+by (rtac refl 1);
 qed "zabs_number_of";
 
 (*0 and 1 require special rewrites because they aren't numerals*)
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/Integ/IntArith.ML
--- a/src/HOL/Integ/IntArith.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/Integ/IntArith.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -10,17 +10,17 @@
 Addsimps [int_diff_minus_eq];
 
 Goal "abs(abs(x::int)) = abs(x)";
-by(arith_tac 1);
+by (arith_tac 1);
 qed "abs_abs";
 Addsimps [abs_abs];
 
 Goal "abs(-(x::int)) = abs(x)";
-by(arith_tac 1);
+by (arith_tac 1);
 qed "abs_minus";
 Addsimps [abs_minus];
 
 Goal "abs(x+y) <= abs(x) + abs(y::int)";
-by(arith_tac 1);
+by (arith_tac 1);
 qed "triangle_ineq";
 
 
@@ -28,35 +28,35 @@
 
 Goal "(ALL i<n::nat. abs(f(i+1) - f i) <= 1) --> \
 \     f 0 <= k --> k <= f n --> (EX i <= n. f i = (k::int))";
-by(induct_tac "n" 1);
- by(Asm_simp_tac 1);
-by(strip_tac 1);
-by(etac impE 1);
- by(Asm_full_simp_tac 1);
-by(eres_inst_tac [("x","n")] allE 1);
-by(Asm_full_simp_tac 1);
-by(case_tac "k = f(n+1)" 1);
- by(Force_tac 1);
-by(etac impE 1);
- by(asm_full_simp_tac (simpset() addsimps [zabs_def] 
+by (induct_tac "n" 1);
+ by (Asm_simp_tac 1);
+by (strip_tac 1);
+by (etac impE 1);
+ by (Asm_full_simp_tac 1);
+by (eres_inst_tac [("x","n")] allE 1);
+by (Asm_full_simp_tac 1);
+by (case_tac "k = f(n+1)" 1);
+ by (Force_tac 1);
+by (etac impE 1);
+ by (asm_full_simp_tac (simpset() addsimps [zabs_def] 
                                  addsplits [split_if_asm]) 1);
- by(arith_tac 1);
-by(blast_tac (claset() addIs [le_SucI]) 1);
+ by (arith_tac 1);
+by (blast_tac (claset() addIs [le_SucI]) 1);
 val lemma = result();
 
 bind_thm("nat0_intermed_int_val", ObjectLogic.rulify_no_asm lemma);
 
 Goal "[| !i. m <= i & i < n --> abs(f(i + 1::nat) - f i) <= 1; m < n; \
 \        f m <= k; k <= f n |] ==> ? i. m <= i & i <= n & f i = (k::int)";
-by(cut_inst_tac [("n","n-m"),("f", "%i. f(i+m)"),("k","k")]lemma 1);
-by(Asm_full_simp_tac 1);
-by(etac impE 1);
- by(strip_tac 1);
- by(eres_inst_tac [("x","i+m")] allE 1);
- by(arith_tac 1);
-by(etac exE 1);
-by(res_inst_tac [("x","i+m")] exI 1);
-by(arith_tac 1);
+by (cut_inst_tac [("n","n-m"),("f", "%i. f(i+m)"),("k","k")]lemma 1);
+by (Asm_full_simp_tac 1);
+by (etac impE 1);
+ by (strip_tac 1);
+ by (eres_inst_tac [("x","i+m")] allE 1);
+ by (arith_tac 1);
+by (etac exE 1);
+by (res_inst_tac [("x","i+m")] exI 1);
+by (arith_tac 1);
 qed "nat_intermed_int_val";
 
 
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/Integ/NatSimprocs.ML
--- a/src/HOL/Integ/NatSimprocs.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/Integ/NatSimprocs.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -101,7 +101,7 @@
 Goal "Suc(Suc(m)) mod 2 = m mod 2";
 by (subgoal_tac "m mod 2 < 2" 1);
 by (Asm_simp_tac 2);
-be (less_2_cases RS disjE) 1;
+by (etac (less_2_cases RS disjE) 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [Let_def, mod_Suc, nat_1])));
 qed "mod2_Suc_Suc";
 Addsimps [mod2_Suc_Suc];
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/Integ/int_arith2.ML
--- a/src/HOL/Integ/int_arith2.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/Integ/int_arith2.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -98,7 +98,7 @@
 
 Goalw [zabs_def]
  "P(abs(i::int)) = ((0 <= i --> P i) & (i < 0 --> P(-i)))";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "zabs_split";
 
 Goal "0 <= abs (z::int)";
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/Lex/AutoChopper.ML
--- a/src/HOL/Lex/AutoChopper.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/Lex/AutoChopper.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -202,8 +202,8 @@
    by (asm_simp_tac HOL_ss 1);
   by (res_inst_tac [("x","x")] exI 1);
   by (Asm_simp_tac 1);
-  by(rtac allI 1);
-  by(case_tac "as" 1);
+  by (rtac allI 1);
+  by (case_tac "as" 1);
    by (Asm_simp_tac 1);
   by (asm_simp_tac (simpset() addcongs[conj_cong]) 1);
  by (strip_tac 1);
@@ -214,8 +214,8 @@
   by (asm_simp_tac HOL_ss 1);
  by (res_inst_tac [("x","x")] exI 1);
  by (Asm_simp_tac 1);
- by(rtac allI 1);
- by(case_tac "as" 1);
+ by (rtac allI 1);
+ by (case_tac "as" 1);
   by (Asm_simp_tac 1);
  by (asm_simp_tac (simpset() addcongs[conj_cong]) 1);
 by (Asm_simp_tac 1);
@@ -225,8 +225,8 @@
  by (subgoal_tac "r @ [a] ~= []" 1);
   by (Fast_tac 1);
  by (Simp_tac 1);
-by(rtac allI 1);
-by(case_tac "as" 1);
+by (rtac allI 1);
+by (case_tac "as" 1);
  by (Asm_simp_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [acc_prefix_def] addcongs[conj_cong]) 1);
 by (etac thin_rl 1); (* speed up *)
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/List.ML
--- a/src/HOL/List.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/List.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -49,8 +49,8 @@
 Addsimps [lists_Int_eq];
 
 Goal "(xs@ys : lists A) = (xs : lists A & ys : lists A)";
-by(induct_tac "xs" 1);
-by(Auto_tac);
+by (induct_tac "xs" 1);
+by (Auto_tac);
 qed "append_in_lists_conv";
 AddIffs [append_in_lists_conv];
 
@@ -725,7 +725,7 @@
 qed_spec_mp "set_update_subset_insert";
 
 Goal "[| set xs <= A; x:A |] ==> set(xs[i := x]) <= A";
-by(fast_tac (claset() addSDs [set_update_subset_insert RS subsetD]) 1);
+by (fast_tac (claset() addSDs [set_update_subset_insert RS subsetD]) 1);
 qed "set_update_subsetI";
 
 (** last & butlast **)
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/Nat.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -47,7 +47,7 @@
 bind_thm ("gr0I", [neq0_conv, notI] MRS iffD1);
 
 Goal "(0<n) = (EX m. n = Suc m)";
-by(fast_tac (claset() addIs [not0_implies_Suc]) 1);
+by (fast_tac (claset() addIs [not0_implies_Suc]) 1);
 qed "gr0_conv_Suc";
 
 Goal "!!n::nat. (~(0 < n)) = (n=0)";
@@ -654,7 +654,7 @@
 Addsimps [mult_eq_1_iff];
 
 Goal "(Suc 0 = m*n) = (m=1 & n=1)";
-by(rtac (mult_eq_1_iff RSN (2,trans)) 1);
+by (rtac (mult_eq_1_iff RSN (2,trans)) 1);
 by (fast_tac (claset() addss simpset()) 1);
 qed "one_eq_mult_iff";
 Addsimps [one_eq_mult_iff];
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/Prolog/Func.ML
--- a/src/HOL/Prolog/Func.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/Prolog/Func.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -1,7 +1,7 @@
 open Func;
 
 val prog_Func = prog_HOHH @ [eval];
-fun pgoal s = (case Goal s of _ => by(prolog_tac prog_Func));
+fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Func));
 val p = ptac prog_Func 1;
 
 pgoal "eval ((S (S Z)) + (S Z)) ?X";
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/Prolog/Test.ML
--- a/src/HOL/Prolog/Test.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/Prolog/Test.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -1,7 +1,7 @@
 open Test;
 
 val prog_Test = prog_HOHH@[append, reverse, mappred, mapfun, age, eq, bag_appl];
-fun pgoal s = (case Goal s of _ => by(prolog_tac prog_Test));
+fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Test));
 val p = ptac prog_Test 1;
 
 pgoal "append ?x ?y [a,b,c,d]";
@@ -40,8 +40,8 @@
 
 (*
 goal thy "f a = ?g a a & ?g = x"; 
-by(rtac conjI 1);
-by(rtac refl 1);
+by (rtac conjI 1);
+by (rtac refl 1);
 back();
 back();
 *)
@@ -103,19 +103,19 @@
 
 (* implication and disjunction in atom: *)
 goal thy "? Q. (!p q. R(q :- p) => R(Q p q)) & Q (t | s) (s | t)";
-by(fast_tac HOL_cs 1);
+by (fast_tac HOL_cs 1);
 
 (* disjunction in atom: *)
 goal thy "(!P. g P :- (P => b | a)) => g(a | b)";
-by(step_tac HOL_cs 1);
-by(step_tac HOL_cs 1);
-by(step_tac HOL_cs 1);
-by(fast_tac HOL_cs 2);
-by(fast_tac HOL_cs 1);
+by (step_tac HOL_cs 1);
+by (step_tac HOL_cs 1);
+by (step_tac HOL_cs 1);
+by (fast_tac HOL_cs 2);
+by (fast_tac HOL_cs 1);
 (*
 hangs:
 goal thy "(!P. g P :- (P => b | a)) => g(a | b)";
-by(fast_tac HOL_cs 1);
+by (fast_tac HOL_cs 1);
 *)
 
 pgoal "!Emp Stk.(\
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/Prolog/Type.ML
--- a/src/HOL/Prolog/Type.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/Prolog/Type.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -1,5 +1,5 @@
 val prog_Type = prog_Func @ [good_typeof,common_typeof];
-fun pgoal s = (case Goal s of _ => by(prolog_tac prog_Type));
+fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Type));
 val p = ptac prog_Type 1;
 
 pgoal "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T";
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/Transitive_Closure_lemmas.ML
--- a/src/HOL/Transitive_Closure_lemmas.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/Transitive_Closure_lemmas.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -305,7 +305,7 @@
 qed "converse_trancl_induct";
 
 Goal "(x,y):R^+ ==> ? z. (x,z):R & (z,y):R^*";
-be converse_trancl_induct 1;
+by (etac converse_trancl_induct 1);
 by Auto_tac;
 by (blast_tac (claset() addIs [rtrancl_trans]) 1);
 qed "tranclD";
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/Wellfounded_Recursion.ML
--- a/src/HOL/Wellfounded_Recursion.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/Wellfounded_Recursion.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -222,7 +222,7 @@
 AddIffs [acyclic_converse];
 
 Goalw [acyclic_def,antisym_def] "acyclic r ==> antisym(r^*)";
-by(blast_tac (claset() addEs [rtranclE]
+by (blast_tac (claset() addEs [rtranclE]
      addIs [rtrancl_into_trancl1,rtrancl_trancl_trancl]) 1);
 qed "acyclic_impl_antisym_rtrancl";
 
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/Wellfounded_Relations.ML
--- a/src/HOL/Wellfounded_Relations.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/Wellfounded_Relations.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -174,12 +174,12 @@
 
 val prems = goalw thy [same_fst_def]
   "(!!x. P x ==> wf(R x)) ==> wf(same_fst P R)";
-by(full_simp_tac (simpset() delcongs [imp_cong] addsimps [wf_def]) 1);
-by(strip_tac 1);
-by(rename_tac "a b" 1);
-by(case_tac "wf(R a)" 1);
+by (full_simp_tac (simpset() delcongs [imp_cong] addsimps [wf_def]) 1);
+by (strip_tac 1);
+by (rename_tac "a b" 1);
+by (case_tac "wf(R a)" 1);
  by (eres_inst_tac [("a","b")] wf_induct 1);
  by (EVERY1[etac allE, etac allE, etac mp, rtac allI, rtac allI]);
- by(Blast_tac 1);
-by(blast_tac (claset() addIs prems) 1);
+ by (Blast_tac 1);
+by (blast_tac (claset() addIs prems) 1);
 qed "wf_same_fst";
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/equalities.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -427,12 +427,12 @@
 Addsimps [Compl_UNIV_eq, Compl_empty_eq];
 
 Goal "(-A <= -B) = (B <= (A::'a set))";
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed "Compl_subset_Compl_iff";
 AddIffs [Compl_subset_Compl_iff];
 
 Goal "(-A = -B) = (A = (B::'a set))";
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed "Compl_eq_Compl_iff";
 AddIffs [Compl_eq_Compl_iff];
 
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/ex/AVL.ML
--- a/src/HOL/ex/AVL.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/ex/AVL.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -129,15 +129,15 @@
  by (case_tac "height (insert x tree1) = Suc (Suc (height tree2))" 1);
   by (forw_inst_tac [("n","nat")]  height_l_bal 1);  
   by (asm_full_simp_tac (simpset() addsimps [max_def]) 1);
-  by(fast_tac (claset() addss simpset()) 1);
+  by (fast_tac (claset() addss simpset()) 1);
  by (asm_full_simp_tac (simpset() addsimps [max_def]) 1);
- by(fast_tac (claset() addss simpset()) 1);
+ by (fast_tac (claset() addss simpset()) 1);
 by (case_tac "height (insert x tree2) = Suc (Suc (height tree1))" 1);
  by (forw_inst_tac [("n","nat")]  height_r_bal 1); 
  by (asm_full_simp_tac (simpset() addsimps [max_def]) 1);
- by(fast_tac (claset() addss simpset()) 1);
+ by (fast_tac (claset() addss simpset()) 1);
 by (asm_full_simp_tac (simpset() addsimps [max_def]) 1);
-by(fast_tac (claset() addss simpset()) 1);
+by (fast_tac (claset() addss simpset()) 1);
 qed_spec_mp "height_insert";
 
 
@@ -174,9 +174,9 @@
   by (fast_tac (claset() addIs [isbal_r_rot] addss (simpset() 
 	addsimps [l_bal_def])) 1);  
  by (Clarify_tac 1);
- by (forward_tac [isbal_insert_left] 1);
+ by (ftac isbal_insert_left 1);
    by (Asm_full_simp_tac 1); 
-  ba 1;
+  by (assume_tac 1);
  by (Asm_full_simp_tac 1); 
 by (case_tac "height (insert x tree2) = Suc (Suc (height tree1))" 1);
  by (case_tac "bal (insert x tree2) = Left" 1);
@@ -185,9 +185,9 @@
  by (fast_tac (claset() addIs [isbal_l_rot] addss (simpset() 
 	addsimps [r_bal_def])) 1);  
 by (Clarify_tac 1);
-by (forward_tac [isbal_insert_right] 1);
+by (ftac isbal_insert_right 1);
    by (Asm_full_simp_tac 1); 
-  ba 1;
+  by (assume_tac 1);
  by (Asm_full_simp_tac 1); 
 qed_spec_mp "isbal_insert";
 
@@ -243,9 +243,9 @@
 "isin y (insert x t) = (y=x | isin y t)";
 by (induct_tac "t" 1);
  by (Asm_simp_tac 1);
-by(asm_simp_tac (simpset() addsimps [l_bal_def,isin_lr_rot,isin_r_rot,
+by (asm_simp_tac (simpset() addsimps [l_bal_def,isin_lr_rot,isin_r_rot,
 	r_bal_def,isin_rl_rot,isin_l_rot]) 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed "isin_insert";
 
 
@@ -261,7 +261,7 @@
 by (case_tac "tree2" 1);
  by (Asm_simp_tac 1);
 by (Asm_simp_tac 1);
-by(blast_tac (claset() addIs [less_trans])1);
+by (blast_tac (claset() addIs [less_trans])1);
 qed_spec_mp "isord_lr_rot";
 
 
@@ -282,7 +282,7 @@
 by (case_tac "tree1" 1);
  by (asm_simp_tac (simpset() addsimps [le_def]) 1);
 by (Asm_simp_tac 1);
-by(blast_tac (claset() addIs [less_trans])1);
+by (blast_tac (claset() addIs [less_trans])1);
 qed_spec_mp "isord_rl_rot";
 
 
@@ -292,7 +292,7 @@
 by (case_tac "r" 1); 
  by (Asm_simp_tac 1);
 by (Asm_simp_tac 1);
-by(blast_tac (claset() addIs [less_trans])1);
+by (blast_tac (claset() addIs [less_trans])1);
 qed_spec_mp "isord_l_rot";
 
 (* insert operation presreves isord property *)
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/ex/Puzzle.ML
--- a/src/HOL/ex/Puzzle.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/ex/Puzzle.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -32,9 +32,9 @@
  by (Simp_tac 1);
 by (rtac impI 1);
 by (etac le_SucE 1);
- by(cut_inst_tac [("n","n")]lemma2 1);
- by(arith_tac 1);
-by(Asm_simp_tac 1);
+ by (cut_inst_tac [("n","n")]lemma2 1);
+ by (arith_tac 1);
+by (Asm_simp_tac 1);
 qed_spec_mp "f_mono";
 
 Goal "f(n) = n";
diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/ex/Sorting.ML
--- a/src/HOL/ex/Sorting.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/ex/Sorting.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -28,7 +28,7 @@
 Goal "transf(le) ==> sorted1 le xs = sorted le xs";
 by (induct_tac "xs" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsplits [list.split])));
-by (rewrite_goals_tac [transf_def]);
+by (rewtac transf_def);
 by (Blast_tac 1);
 qed "sorted1_is_sorted";