Ran expandshort
authorpaulson
Thu Sep 26 12:47:47 1996 +0200 (1996-09-26)
changeset 203103a843f0f447
parent 2030 474b3f208789
child 2032 1bbf1bdcaf56
Ran expandshort
src/HOL/Arith.ML
src/HOL/Finite.ML
src/HOL/Fun.ML
src/HOL/HOL.ML
src/HOL/Hoare/Arith2.ML
src/HOL/Hoare/Examples.ML
src/HOL/Hoare/List_Examples.ML
src/HOL/IMP/Denotation.ML
src/HOL/IMP/Hoare.ML
src/HOL/IMP/Transition.ML
src/HOL/IMP/VC.ML
src/HOL/Lambda/Commutation.ML
src/HOL/Lambda/Eta.ML
src/HOL/Lambda/Lambda.ML
src/HOL/Lambda/ParRed.ML
src/HOL/MiniML/I.ML
src/HOL/MiniML/Maybe.ML
src/HOL/MiniML/MiniML.ML
src/HOL/MiniML/ROOT.ML
src/HOL/MiniML/Type.ML
src/HOL/MiniML/W.ML
src/HOL/Nat.ML
src/HOL/Option.ML
src/HOL/Prod.ML
src/HOL/RelPow.ML
src/HOL/Relation.ML
src/HOL/Set.ML
src/HOL/Sexp.ML
src/HOL/Trancl.ML
src/HOL/WF.ML
src/HOL/datatype.ML
src/HOL/equalities.ML
src/HOL/ex/Comb.ML
src/HOL/ex/InSort.ML
src/HOL/ex/LList.ML
src/HOL/ex/LexProd.ML
src/HOL/ex/Mutil.ML
src/HOL/ex/PropLog.ML
src/HOL/ex/Puzzle.ML
src/HOL/ex/Qsort.ML
src/HOL/ex/SList.ML
src/HOL/ex/Sorting.ML
src/HOL/ex/String.ML
src/HOL/ex/meson.ML
src/HOL/ex/mesontest.ML
src/HOL/ex/set.ML
src/HOL/ex/unsolved.ML
src/HOL/indrule.ML
src/HOL/intr_elim.ML
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/Arith.ML	Thu Sep 26 11:11:22 1996 +0200
     1.2 +++ b/src/HOL/Arith.ML	Thu Sep 26 12:47:47 1996 +0200
     1.3 @@ -164,7 +164,7 @@
     1.4  (*Associative law for multiplication*)
     1.5  qed_goal "mult_assoc" Arith.thy "(m * n) * k = m * ((n * k)::nat)"
     1.6    (fn _ => [nat_ind_tac "m" 1, 
     1.7 -	    ALLGOALS (asm_simp_tac (!simpset addsimps [add_mult_distrib]))]);
     1.8 +            ALLGOALS (asm_simp_tac (!simpset addsimps [add_mult_distrib]))]);
     1.9  
    1.10  qed_goal "mult_left_commute" Arith.thy "x*(y*z) = y*((x*z)::nat)"
    1.11   (fn _ => [rtac trans 1, rtac mult_commute 1, rtac trans 1,
    1.12 @@ -539,7 +539,7 @@
    1.13  
    1.14  (*strict, in 1st argument; proof is by induction on k>0*)
    1.15  goal Arith.thy "!!i::nat. [| i<j; 0<k |] ==> k*i < k*j";
    1.16 -be zero_less_natE 1;
    1.17 +by (etac zero_less_natE 1);
    1.18  by (Asm_simp_tac 1);
    1.19  by (nat_ind_tac "x" 1);
    1.20  by (ALLGOALS (asm_simp_tac (!simpset addsimps [add_less_mono])));
    1.21 @@ -564,26 +564,26 @@
    1.22  by (res_inst_tac [("n","m")] less_induct 1);
    1.23  by (case_tac "na<n" 1);
    1.24  by (asm_simp_tac (!simpset addsimps [div_less, zero_less_mult_iff, 
    1.25 -				     mult_less_mono2]) 1);
    1.26 +                                     mult_less_mono2]) 1);
    1.27  by (subgoal_tac "~ k*na < k*n" 1);
    1.28  by (asm_simp_tac
    1.29       (!simpset addsimps [zero_less_mult_iff, div_geq,
    1.30 -			 diff_mult_distrib2 RS sym, diff_less]) 1);
    1.31 +                         diff_mult_distrib2 RS sym, diff_less]) 1);
    1.32  by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le, 
    1.33 -					  le_refl RS mult_le_mono]) 1);
    1.34 +                                          le_refl RS mult_le_mono]) 1);
    1.35  qed "div_cancel";
    1.36  
    1.37  goal Arith.thy "!!k. [| 0<n; 0<k |] ==> (k*m) mod (k*n) = k * (m mod n)";
    1.38  by (res_inst_tac [("n","m")] less_induct 1);
    1.39  by (case_tac "na<n" 1);
    1.40  by (asm_simp_tac (!simpset addsimps [mod_less, zero_less_mult_iff, 
    1.41 -				     mult_less_mono2]) 1);
    1.42 +                                     mult_less_mono2]) 1);
    1.43  by (subgoal_tac "~ k*na < k*n" 1);
    1.44  by (asm_simp_tac
    1.45       (!simpset addsimps [zero_less_mult_iff, mod_geq,
    1.46 -			 diff_mult_distrib2 RS sym, diff_less]) 1);
    1.47 +                         diff_mult_distrib2 RS sym, diff_less]) 1);
    1.48  by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le, 
    1.49 -					  le_refl RS mult_le_mono]) 1);
    1.50 +                                          le_refl RS mult_le_mono]) 1);
    1.51  qed "mult_mod_distrib";
    1.52  
    1.53  
     2.1 --- a/src/HOL/Finite.ML	Thu Sep 26 11:11:22 1996 +0200
     2.2 +++ b/src/HOL/Finite.ML	Thu Sep 26 12:47:47 1996 +0200
     2.3 @@ -74,7 +74,7 @@
     2.4  by (Simp_tac 1);
     2.5  by (asm_simp_tac
     2.6      (!simpset addsimps [image_eqI RS Fin.insertI, image_insert]
     2.7 -	      delsimps [insert_Fin]) 1);
     2.8 +              delsimps [insert_Fin]) 1);
     2.9  qed "Fin_imageI";
    2.10  
    2.11  val major::prems = goal Finite.thy 
    2.12 @@ -83,7 +83,7 @@
    2.13  \       !!(x::'a) y. [| x:A; y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
    2.14  \    |] ==> c<=b --> P(b-c)";
    2.15  by (rtac (major RS Fin_induct) 1);
    2.16 -by (rtac (Diff_insert RS ssubst) 2);
    2.17 +by (stac Diff_insert 2);
    2.18  by (ALLGOALS (asm_simp_tac
    2.19                  (!simpset addsimps (prems@[Diff_subset RS Fin_subset]))));
    2.20  val lemma = result();
    2.21 @@ -259,7 +259,7 @@
    2.22     [("x","%i. if i<(LEAST n. ? f. A={f i |i. i < n}) then f i else x")] exI 1);
    2.23   by (simp_tac
    2.24      (!simpset addsimps [Collect_conv_insert, less_Suc_eq] 
    2.25 -	      addcongs [rev_conj_cong]) 1);
    2.26 +              addcongs [rev_conj_cong]) 1);
    2.27   be subst 1;
    2.28   br refl 1;
    2.29  by (rtac notI 1);
    2.30 @@ -290,7 +290,7 @@
    2.31  qed "card_Suc_Diff";
    2.32  
    2.33  goal Finite.thy "!!A. [| finite A; x: A |] ==> card(A-{x}) < card A";
    2.34 -by (resolve_tac [Suc_less_SucD] 1);
    2.35 +by (rtac Suc_less_SucD 1);
    2.36  by (asm_simp_tac (!simpset addsimps [card_Suc_Diff]) 1);
    2.37  qed "card_Diff";
    2.38  
     3.1 --- a/src/HOL/Fun.ML	Thu Sep 26 11:11:22 1996 +0200
     3.2 +++ b/src/HOL/Fun.ML	Thu Sep 26 12:47:47 1996 +0200
     3.3 @@ -173,7 +173,7 @@
     3.4              ComplI, IntI, DiffI, UnCI, insertCI]; 
     3.5  AddIs  [bexI, UnionI, UN_I, UN1_I, imageI, rangeI]; 
     3.6  AddSEs [bexE, make_elim PowD, UnionE, UN_E, UN1_E, DiffE,
     3.7 -	    make_elim singleton_inject,
     3.8 +            make_elim singleton_inject,
     3.9              CollectE, ComplE, IntE, UnE, insertE, imageE, rangeE, emptyE]; 
    3.10  AddEs  [ballE, InterD, InterE, INT_D, INT_E, make_elim INT1_D,
    3.11              subsetD, subsetCE];
     4.1 --- a/src/HOL/HOL.ML	Thu Sep 26 11:11:22 1996 +0200
     4.2 +++ b/src/HOL/HOL.ML	Thu Sep 26 12:47:47 1996 +0200
     4.3 @@ -214,22 +214,22 @@
     4.4    [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]);
     4.5  
     4.6  qed_goal "contrapos2" HOL.thy "[| Q; ~ P ==> ~ Q |] ==> P" (fn [p1,p2] => [
     4.7 -	rtac classical 1,
     4.8 -	dtac p2 1,
     4.9 -	etac notE 1,
    4.10 -	rtac p1 1]);
    4.11 +        rtac classical 1,
    4.12 +        dtac p2 1,
    4.13 +        etac notE 1,
    4.14 +        rtac p1 1]);
    4.15  
    4.16  qed_goal "swap2" HOL.thy "[| P;  Q ==> ~ P |] ==> ~ Q" (fn [p1,p2] => [
    4.17 -	rtac notI 1,
    4.18 -	dtac p2 1,
    4.19 -	etac notE 1,
    4.20 -	rtac p1 1]);
    4.21 +        rtac notI 1,
    4.22 +        dtac p2 1,
    4.23 +        etac notE 1,
    4.24 +        rtac p1 1]);
    4.25  
    4.26  (** Unique existence **)
    4.27  section "?!";
    4.28  
    4.29  qed_goalw "ex1I" HOL.thy [Ex1_def]
    4.30 -	    "[| P(a);  !!x. P(x) ==> x=a |] ==> ?! x. P(x)"
    4.31 +            "[| P(a);  !!x. P(x) ==> x=a |] ==> ?! x. P(x)"
    4.32   (fn prems =>
    4.33    [REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)]);
    4.34  
     5.1 --- a/src/HOL/Hoare/Arith2.ML	Thu Sep 26 11:11:22 1996 +0200
     5.2 +++ b/src/HOL/Hoare/Arith2.ML	Thu Sep 26 12:47:47 1996 +0200
     5.3 @@ -30,16 +30,16 @@
     5.4  \       !!x y z. [| P x y z |] ==> P (Suc x) (Suc y) (Suc z)  \
     5.5  \    |] ==> P m n k";
     5.6  by (res_inst_tac [("x","m")] spec 1);
     5.7 -br diff_induct 1;
     5.8 -br allI 1;
     5.9 -br allI 2;
    5.10 +by (rtac diff_induct 1);
    5.11 +by (rtac allI 1);
    5.12 +by (rtac allI 2);
    5.13  by (res_inst_tac [("m","xa"),("n","x")] diff_induct 1);
    5.14  by (res_inst_tac [("m","x"),("n","Suc y")] diff_induct 4);
    5.15 -br allI 7;
    5.16 +by (rtac allI 7);
    5.17  by (nat_ind_tac "xa" 7);
    5.18  by (ALLGOALS (resolve_tac prems));
    5.19 -ba 1;
    5.20 -ba 1;
    5.21 +by (assume_tac 1);
    5.22 +by (assume_tac 1);
    5.23  by (Fast_tac 1);
    5.24  by (Fast_tac 1);
    5.25  qed "diff_induct3";
    5.26 @@ -48,33 +48,33 @@
    5.27  
    5.28  val prems=goal Arith.thy "~m<n+k ==> (m - n) - k = m - ((n + k)::nat)";
    5.29  by (cut_facts_tac prems 1);
    5.30 -br mp 1;
    5.31 -ba 2;
    5.32 +by (rtac mp 1);
    5.33 +by (assume_tac 2);
    5.34  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    5.35  by (ALLGOALS Asm_simp_tac);
    5.36  qed "diff_not_assoc";
    5.37  
    5.38  val prems=goal Arith.thy "[|~m<n; ~n<k|] ==> (m - n) + k = m - ((n - k)::nat)";
    5.39  by (cut_facts_tac prems 1);
    5.40 -bd conjI 1;
    5.41 -ba 1;
    5.42 +by (dtac conjI 1);
    5.43 +by (assume_tac 1);
    5.44  by (res_inst_tac [("P","~m<n & ~n<k")] mp 1);
    5.45 -ba 2;
    5.46 +by (assume_tac 2);
    5.47  by (res_inst_tac [("m","m"),("n","n"),("k","k")] diff_induct3 1);
    5.48  by (ALLGOALS Asm_simp_tac);
    5.49 -br impI 1;
    5.50 +by (rtac impI 1);
    5.51  by (dres_inst_tac [("P","~x<y")] conjE 1);
    5.52 -ba 2;
    5.53 -br (Suc_diff_n RS sym) 1;
    5.54 -br le_less_trans 1;
    5.55 -be (not_less_eq RS subst) 2;
    5.56 -br (hd ([diff_less_Suc RS lessD] RL [Suc_le_mono RS subst])) 1;
    5.57 +by (assume_tac 2);
    5.58 +by (rtac (Suc_diff_n RS sym) 1);
    5.59 +by (rtac le_less_trans 1);
    5.60 +by (etac (not_less_eq RS subst) 2);
    5.61 +by (rtac (hd ([diff_less_Suc RS lessD] RL [Suc_le_mono RS subst])) 1);
    5.62  qed "diff_add_not_assoc";
    5.63  
    5.64  val prems=goal Arith.thy "~n<k ==> (m + n) - k = m + ((n - k)::nat)";
    5.65  by (cut_facts_tac prems 1);
    5.66 -br mp 1;
    5.67 -ba 2;
    5.68 +by (rtac mp 1);
    5.69 +by (assume_tac 2);
    5.70  by (res_inst_tac [("m","n"),("n","k")] diff_induct 1);
    5.71  by (ALLGOALS Asm_simp_tac);
    5.72  qed "add_diff_assoc";
    5.73 @@ -82,12 +82,12 @@
    5.74  (*** more ***)
    5.75  
    5.76  val prems = goal Arith.thy "m~=(n::nat) = (m<n | n<m)";
    5.77 -br iffI 1;
    5.78 +by (rtac iffI 1);
    5.79  by (cut_inst_tac [("m","m"),("n","n")] less_linear 1);
    5.80  by (Asm_full_simp_tac 1);
    5.81 -be disjE 1;
    5.82 -be (less_not_refl2 RS not_sym) 1;
    5.83 -be less_not_refl2 1;
    5.84 +by (etac disjE 1);
    5.85 +by (etac (less_not_refl2 RS not_sym) 1);
    5.86 +by (etac less_not_refl2 1);
    5.87  qed "not_eq_eq_less_or_gr";
    5.88  
    5.89  val [prem] = goal Arith.thy "m<n ==> n-m~=0";
    5.90 @@ -117,7 +117,7 @@
    5.91  by (res_inst_tac [("n","k")] natE 1);
    5.92  by (ALLGOALS Asm_full_simp_tac);
    5.93  by (nat_ind_tac "x" 1);
    5.94 -be add_less_mono 2;
    5.95 +by (etac add_less_mono 2);
    5.96  by (ALLGOALS Asm_full_simp_tac);
    5.97  qed "mult_less_mono_r";
    5.98  
    5.99 @@ -126,8 +126,8 @@
   5.100  by (nat_ind_tac "k" 1);
   5.101  by (ALLGOALS Simp_tac);
   5.102  by (fold_goals_tac [le_def]);
   5.103 -be add_le_mono 1;
   5.104 -ba 1;
   5.105 +by (etac add_le_mono 1);
   5.106 +by (assume_tac 1);
   5.107  qed "mult_not_less_mono_r";
   5.108  
   5.109  val prems = goal Arith.thy "m=(n::nat) ==> m*k=n*k";
   5.110 @@ -139,10 +139,10 @@
   5.111  val prems = goal Arith.thy "[|0<k; m~=(n::nat)|] ==> m*k~=n*k";
   5.112  by (cut_facts_tac prems 1);
   5.113  by (res_inst_tac [("P","m<n"),("Q","n<m")] disjE 1);
   5.114 -br (less_not_refl2 RS not_sym) 2;
   5.115 -be mult_less_mono_r 2;
   5.116 -br less_not_refl2 3;
   5.117 -be mult_less_mono_r 3;
   5.118 +by (rtac (less_not_refl2 RS not_sym) 2);
   5.119 +by (etac mult_less_mono_r 2);
   5.120 +by (rtac less_not_refl2 3);
   5.121 +by (etac mult_less_mono_r 3);
   5.122  by (ALLGOALS (asm_full_simp_tac ((simpset_of "Arith") addsimps [not_eq_eq_less_or_gr])));
   5.123  qed "mult_not_eq_mono_r";
   5.124  
   5.125 @@ -166,29 +166,29 @@
   5.126  
   5.127  val prems=goal thy "0<n ==> n mod n = 0";
   5.128  by (cut_facts_tac prems 1);
   5.129 -br (mod_def RS wf_less_trans) 1;
   5.130 +by (rtac (mod_def RS wf_less_trans) 1);
   5.131  by (asm_full_simp_tac ((simpset_of "Arith") addsimps [diff_self_eq_0,cut_def,less_eq]) 1);
   5.132 -be mod_less 1;
   5.133 +by (etac mod_less 1);
   5.134  qed "mod_nn_is_0";
   5.135  
   5.136  val prems=goal thy "0<n ==> m mod n = (m+n) mod n";
   5.137  by (cut_facts_tac prems 1);
   5.138  by (res_inst_tac [("s","n+m"),("t","m+n")] subst 1);
   5.139 -br add_commute 1;
   5.140 +by (rtac add_commute 1);
   5.141  by (res_inst_tac [("s","n+m-n"),("P","%x.x mod n = (n + m) mod n")] subst 1);
   5.142 -br diff_add_inverse 1;
   5.143 -br sym 1;
   5.144 -be mod_geq 1;
   5.145 +by (rtac diff_add_inverse 1);
   5.146 +by (rtac sym 1);
   5.147 +by (etac mod_geq 1);
   5.148  by (res_inst_tac [("s","n<=n+m"),("t","~n+m<n")] subst 1);
   5.149  by (simp_tac ((simpset_of "Arith") addsimps [le_def]) 1);
   5.150 -br le_add1 1;
   5.151 +by (rtac le_add1 1);
   5.152  qed "mod_eq_add";
   5.153  
   5.154  val prems=goal thy "0<n ==> m*n mod n = 0";
   5.155  by (cut_facts_tac prems 1);
   5.156  by (nat_ind_tac "m" 1);
   5.157  by (Simp_tac 1);
   5.158 -be mod_less 1;
   5.159 +by (etac mod_less 1);
   5.160  by (dres_inst_tac [("n","n"),("m","m1*n")] mod_eq_add 1);
   5.161  by (asm_full_simp_tac ((simpset_of "Arith") addsimps [add_commute]) 1);
   5.162  qed "mod_prod_nn_is_0";
   5.163 @@ -196,25 +196,25 @@
   5.164  val prems=goal thy "[|0<x; m mod x = 0; n mod x = 0|] ==> (m+n) mod x = 0";
   5.165  by (cut_facts_tac prems 1);
   5.166  by (res_inst_tac [("s","m div x * x + m mod x"),("t","m")] subst 1);
   5.167 -be mod_div_equality 1;
   5.168 +by (etac mod_div_equality 1);
   5.169  by (res_inst_tac [("s","n div x * x + n mod x"),("t","n")] subst 1);
   5.170 -be mod_div_equality 1;
   5.171 +by (etac mod_div_equality 1);
   5.172  by (Asm_simp_tac 1);
   5.173  by (res_inst_tac [("s","(m div x + n div x) * x"),("t","m div x * x + n div x * x")] subst 1);
   5.174 -br add_mult_distrib 1;
   5.175 -be mod_prod_nn_is_0 1;
   5.176 +by (rtac add_mult_distrib 1);
   5.177 +by (etac mod_prod_nn_is_0 1);
   5.178  qed "mod0_sum";
   5.179  
   5.180  val prems=goal thy "[|0<x; m mod x = 0; n mod x = 0; n<=m|] ==> (m-n) mod x = 0";
   5.181  by (cut_facts_tac prems 1);
   5.182  by (res_inst_tac [("s","m div x * x + m mod x"),("t","m")] subst 1);
   5.183 -be mod_div_equality 1;
   5.184 +by (etac mod_div_equality 1);
   5.185  by (res_inst_tac [("s","n div x * x + n mod x"),("t","n")] subst 1);
   5.186 -be mod_div_equality 1;
   5.187 +by (etac mod_div_equality 1);
   5.188  by (Asm_simp_tac 1);
   5.189  by (res_inst_tac [("s","(m div x - n div x) * x"),("t","m div x * x - n div x * x")] subst 1);
   5.190 -br diff_mult_distrib 1;
   5.191 -be mod_prod_nn_is_0 1;
   5.192 +by (rtac diff_mult_distrib 1);
   5.193 +by (etac mod_prod_nn_is_0 1);
   5.194  qed "mod0_diff";
   5.195  
   5.196  
   5.197 @@ -223,11 +223,11 @@
   5.198  
   5.199  val prems = goal thy "0<n ==> m*n div n = m";
   5.200  by (cut_facts_tac prems 1);
   5.201 -br (mult_not_eq_mono_r RS not_imp_swap) 1;
   5.202 -ba 1;
   5.203 -ba 1;
   5.204 +by (rtac (mult_not_eq_mono_r RS not_imp_swap) 1);
   5.205 +by (assume_tac 1);
   5.206 +by (assume_tac 1);
   5.207  by (res_inst_tac [("P","%x.m*n div n * n = x")] (mod_div_equality RS subst) 1);
   5.208 -ba 1;
   5.209 +by (assume_tac 1);
   5.210  by (dres_inst_tac [("m","m")] mod_prod_nn_is_0 1);
   5.211  by (Asm_simp_tac 1);
   5.212  qed "div_prod_nn_is_m";
   5.213 @@ -243,32 +243,32 @@
   5.214  
   5.215  val prems=goalw thy [divides_def] "x divides n ==> x<=n";
   5.216  by (cut_facts_tac prems 1);
   5.217 -br ((mod_less COMP rev_contrapos) RS (le_def RS meta_eq_to_obj_eq RS iffD2)) 1;
   5.218 +by (rtac ((mod_less COMP rev_contrapos) RS (le_def RS meta_eq_to_obj_eq RS iffD2)) 1);
   5.219  by (Asm_simp_tac 1);
   5.220 -br (less_not_refl2 RS not_sym) 1;
   5.221 +by (rtac (less_not_refl2 RS not_sym) 1);
   5.222  by (Asm_simp_tac 1);
   5.223  qed "divides_le";
   5.224  
   5.225  val prems=goalw thy [divides_def] "[|x divides m; x divides n|] ==> x divides (m+n)";
   5.226  by (cut_facts_tac prems 1);
   5.227  by (REPEAT ((dtac conjE 1) THEN (atac 2)));
   5.228 -br conjI 1;
   5.229 +by (rtac conjI 1);
   5.230  by (dres_inst_tac [("m","0"),("n","m")] less_imp_add_less 1);
   5.231 -ba 1;
   5.232 -be conjI 1;
   5.233 -br mod0_sum 1;
   5.234 +by (assume_tac 1);
   5.235 +by (etac conjI 1);
   5.236 +by (rtac mod0_sum 1);
   5.237  by (ALLGOALS atac);
   5.238  qed "divides_sum";
   5.239  
   5.240  val prems=goalw thy [divides_def] "[|x divides m; x divides n; n<m|] ==> x divides (m-n)";
   5.241  by (cut_facts_tac prems 1);
   5.242  by (REPEAT ((dtac conjE 1) THEN (atac 2)));
   5.243 -br conjI 1;
   5.244 -be less_imp_diff_positive 1;
   5.245 -be conjI 1;
   5.246 -br mod0_diff 1;
   5.247 +by (rtac conjI 1);
   5.248 +by (etac less_imp_diff_positive 1);
   5.249 +by (etac conjI 1);
   5.250 +by (rtac mod0_diff 1);
   5.251  by (ALLGOALS (asm_simp_tac ((simpset_of "Arith") addsimps [le_def])));
   5.252 -be less_not_sym 1;
   5.253 +by (etac less_not_sym 1);
   5.254  qed "divides_diff";
   5.255  
   5.256  
   5.257 @@ -277,16 +277,16 @@
   5.258  
   5.259  val prems=goalw thy [cd_def] "0<n ==> cd n n n";
   5.260  by (cut_facts_tac prems 1);
   5.261 -bd divides_nn 1;
   5.262 +by (dtac divides_nn 1);
   5.263  by (Asm_simp_tac 1);
   5.264  qed "cd_nnn";
   5.265  
   5.266  val prems=goalw thy [cd_def] "cd x m n ==> x<=m & x<=n";
   5.267  by (cut_facts_tac prems 1);
   5.268 -bd conjE 1;
   5.269 -ba 2;
   5.270 -bd divides_le 1;
   5.271 -bd divides_le 1;
   5.272 +by (dtac conjE 1);
   5.273 +by (assume_tac 2);
   5.274 +by (dtac divides_le 1);
   5.275 +by (dtac divides_le 1);
   5.276  by (Asm_simp_tac 1);
   5.277  qed "cd_le";
   5.278  
   5.279 @@ -296,32 +296,32 @@
   5.280  
   5.281  val prems=goalw thy [cd_def] "n<m ==> cd x m n = cd x (m-n) n";
   5.282  by (cut_facts_tac prems 1);
   5.283 -br iffI 1;
   5.284 -bd conjE 1;
   5.285 -ba 2;
   5.286 -br conjI 1;
   5.287 -br divides_diff 1;
   5.288 -bd conjE 5;
   5.289 -ba 6;
   5.290 -br conjI 5;
   5.291 -bd less_not_sym 5;
   5.292 -bd add_diff_inverse 5;
   5.293 +by (rtac iffI 1);
   5.294 +by (dtac conjE 1);
   5.295 +by (assume_tac 2);
   5.296 +by (rtac conjI 1);
   5.297 +by (rtac divides_diff 1);
   5.298 +by (dtac conjE 5);
   5.299 +by (assume_tac 6);
   5.300 +by (rtac conjI 5);
   5.301 +by (dtac less_not_sym 5);
   5.302 +by (dtac add_diff_inverse 5);
   5.303  by (dres_inst_tac [("m","n"),("n","m-n")] divides_sum 5);
   5.304  by (ALLGOALS Asm_full_simp_tac);
   5.305  qed "cd_diff_l";
   5.306  
   5.307  val prems=goalw thy [cd_def] "m<n ==> cd x m n = cd x m (n-m)";
   5.308  by (cut_facts_tac prems 1);
   5.309 -br iffI 1;
   5.310 -bd conjE 1;
   5.311 -ba 2;
   5.312 -br conjI 1;
   5.313 -br divides_diff 2;
   5.314 -bd conjE 5;
   5.315 -ba 6;
   5.316 -br conjI 5;
   5.317 -bd less_not_sym 6;
   5.318 -bd add_diff_inverse 6;
   5.319 +by (rtac iffI 1);
   5.320 +by (dtac conjE 1);
   5.321 +by (assume_tac 2);
   5.322 +by (rtac conjI 1);
   5.323 +by (rtac divides_diff 2);
   5.324 +by (dtac conjE 5);
   5.325 +by (assume_tac 6);
   5.326 +by (rtac conjI 5);
   5.327 +by (dtac less_not_sym 6);
   5.328 +by (dtac add_diff_inverse 6);
   5.329  by (dres_inst_tac [("n","n-m")] divides_sum 6);
   5.330  by (ALLGOALS Asm_full_simp_tac);
   5.331  qed "cd_diff_r";
   5.332 @@ -331,15 +331,15 @@
   5.333  
   5.334  val prems = goalw thy [gcd_def] "0<n ==> n = gcd n n";
   5.335  by (cut_facts_tac prems 1);
   5.336 -bd cd_nnn 1;
   5.337 -br (select_equality RS sym) 1;
   5.338 -be conjI 1;
   5.339 -br allI 1;
   5.340 -br impI 1;
   5.341 -bd cd_le 1;
   5.342 -bd conjE 2;
   5.343 -ba 3;
   5.344 -br le_anti_sym 2;
   5.345 +by (dtac cd_nnn 1);
   5.346 +by (rtac (select_equality RS sym) 1);
   5.347 +by (etac conjI 1);
   5.348 +by (rtac allI 1);
   5.349 +by (rtac impI 1);
   5.350 +by (dtac cd_le 1);
   5.351 +by (dtac conjE 2);
   5.352 +by (assume_tac 3);
   5.353 +by (rtac le_anti_sym 2);
   5.354  by (dres_inst_tac [("x","x")] cd_le 2);
   5.355  by (dres_inst_tac [("x","n")] spec 3);
   5.356  by (ALLGOALS Asm_full_simp_tac);
   5.357 @@ -353,16 +353,16 @@
   5.358  by (cut_facts_tac prems 1);
   5.359  by (subgoal_tac "n<m ==> !x.cd x m n = cd x (m-n) n" 1);
   5.360  by (Asm_simp_tac 1);
   5.361 -br allI 1;
   5.362 -be cd_diff_l 1;
   5.363 +by (rtac allI 1);
   5.364 +by (etac cd_diff_l 1);
   5.365  qed "gcd_diff_l";
   5.366  
   5.367  val prems=goalw thy [gcd_def] "m<n ==> gcd m n = gcd m (n-m)";
   5.368  by (cut_facts_tac prems 1);
   5.369  by (subgoal_tac "m<n ==> !x.cd x m n = cd x m (n-m)" 1);
   5.370  by (Asm_simp_tac 1);
   5.371 -br allI 1;
   5.372 -be cd_diff_r 1;
   5.373 +by (rtac allI 1);
   5.374 +by (etac cd_diff_r 1);
   5.375  qed "gcd_diff_r";
   5.376  
   5.377  
   5.378 @@ -381,7 +381,7 @@
   5.379  by (nat_ind_tac "k" 1);
   5.380  by (ALLGOALS Asm_simp_tac);
   5.381  by (fold_goals_tac [pow_def]);
   5.382 -br (pow_add_reduce RS sym) 1;
   5.383 +by (rtac (pow_add_reduce RS sym) 1);
   5.384  qed "pow_pow_reduce";
   5.385  
   5.386  (*** fac ***)
     6.1 --- a/src/HOL/Hoare/Examples.ML	Thu Sep 26 11:11:22 1996 +0200
     6.2 +++ b/src/HOL/Hoare/Examples.ML	Thu Sep 26 12:47:47 1996 +0200
     6.3 @@ -14,8 +14,8 @@
     6.4   "{m=0 & s=0} \
     6.5  \ WHILE m ~= a DO {s = m*b} s := s+b; m := Suc(m) END\
     6.6  \ {s = a*b}";
     6.7 -by(hoare_tac 1);
     6.8 -by(ALLGOALS (asm_full_simp_tac (!simpset addsimps add_ac)));
     6.9 +by (hoare_tac 1);
    6.10 +by (ALLGOALS (asm_full_simp_tac (!simpset addsimps add_ac)));
    6.11  qed "multiply_by_add";
    6.12  
    6.13  
    6.14 @@ -78,7 +78,7 @@
    6.15  
    6.16  by (subgoal_tac "a*a=a pow 2" 1);
    6.17  by (Asm_simp_tac 1);
    6.18 -by (rtac (pow_pow_reduce RS ssubst) 1);
    6.19 +by (stac pow_pow_reduce 1);
    6.20  
    6.21  by (subgoal_tac "(b div 2)*2=b" 1);
    6.22  by (subgoal_tac "0<2" 2);
     7.1 --- a/src/HOL/Hoare/List_Examples.ML	Thu Sep 26 11:11:22 1996 +0200
     7.2 +++ b/src/HOL/Hoare/List_Examples.ML	Thu Sep 26 12:47:47 1996 +0200
     7.3 @@ -6,11 +6,11 @@
     7.4  \    y := hd x # y; x := tl x \
     7.5  \ END \
     7.6  \{y=rev(X)}";
     7.7 -by(hoare_tac 1);
     7.8 -by(asm_full_simp_tac (!simpset addsimps [neq_Nil_conv]) 1);
     7.9 -by(safe_tac (!claset));
    7.10 -by(Asm_full_simp_tac 1);
    7.11 -by(Asm_full_simp_tac 1);
    7.12 +by (hoare_tac 1);
    7.13 +by (asm_full_simp_tac (!simpset addsimps [neq_Nil_conv]) 1);
    7.14 +by (safe_tac (!claset));
    7.15 +by (Asm_full_simp_tac 1);
    7.16 +by (Asm_full_simp_tac 1);
    7.17  qed "imperative_reverse";
    7.18  
    7.19  goal thy
    7.20 @@ -21,9 +21,9 @@
    7.21  \    y := hd x # y; x := tl x \
    7.22  \ END \
    7.23  \{y = X@Y}";
    7.24 -by(hoare_tac 1);
    7.25 -by(asm_full_simp_tac (!simpset addsimps [neq_Nil_conv]) 1);
    7.26 -by(safe_tac (!claset));
    7.27 -by(Asm_full_simp_tac 1);
    7.28 -by(Asm_full_simp_tac 1);
    7.29 +by (hoare_tac 1);
    7.30 +by (asm_full_simp_tac (!simpset addsimps [neq_Nil_conv]) 1);
    7.31 +by (safe_tac (!claset));
    7.32 +by (Asm_full_simp_tac 1);
    7.33 +by (Asm_full_simp_tac 1);
    7.34  qed "imperative_append";
     8.1 --- a/src/HOL/IMP/Denotation.ML	Thu Sep 26 11:11:22 1996 +0200
     8.2 +++ b/src/HOL/IMP/Denotation.ML	Thu Sep 26 12:47:47 1996 +0200
     8.3 @@ -15,11 +15,11 @@
     8.4  
     8.5  
     8.6  goal Denotation.thy "C(WHILE b DO c) = C(IF b THEN c;WHILE b DO c ELSE SKIP)";
     8.7 -by(Simp_tac 1);
     8.8 -by(EVERY[stac (Gamma_mono RS lfp_Tarski) 1,
     8.9 +by (Simp_tac 1);
    8.10 +by (EVERY[stac (Gamma_mono RS lfp_Tarski) 1,
    8.11            stac (Gamma_def RS meta_eq_to_obj_eq RS fun_cong) 1,
    8.12 -	  Simp_tac 1,
    8.13 -	  IF_UNSOLVED no_tac]);
    8.14 +          Simp_tac 1,
    8.15 +          IF_UNSOLVED no_tac]);
    8.16  qed "C_While_If";
    8.17  
    8.18  
    8.19 @@ -31,7 +31,7 @@
    8.20  by (etac evalc.induct 1);
    8.21  auto();
    8.22  (* while *)
    8.23 -by(rewtac Gamma_def);
    8.24 +by (rewtac Gamma_def);
    8.25  by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1);
    8.26  by (Fast_tac 1);
    8.27  by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1);
    8.28 @@ -44,8 +44,8 @@
    8.29  goal Denotation.thy "!s t. (s,t):C(c) --> <c,s> -c-> t";
    8.30  by (com.induct_tac "c" 1);
    8.31  
    8.32 -by(ALLGOALS Full_simp_tac);
    8.33 -by(ALLGOALS (TRY o Fast_tac));
    8.34 +by (ALLGOALS Full_simp_tac);
    8.35 +by (ALLGOALS (TRY o Fast_tac));
    8.36  
    8.37  (* while *)
    8.38  by (strip_tac 1);
     9.1 --- a/src/HOL/IMP/Hoare.ML	Thu Sep 26 11:11:22 1996 +0200
     9.2 +++ b/src/HOL/IMP/Hoare.ML	Thu Sep 26 12:47:47 1996 +0200
     9.3 @@ -24,38 +24,38 @@
     9.4  qed "hoare_sound";
     9.5  
     9.6  goalw Hoare.thy [swp_def] "swp SKIP Q = Q";
     9.7 -by(Simp_tac 1);
     9.8 -br ext 1;
     9.9 +by (Simp_tac 1);
    9.10 +by (rtac ext 1);
    9.11  by (Fast_tac 1);
    9.12  qed "swp_SKIP";
    9.13  
    9.14  goalw Hoare.thy [swp_def] "swp (x:=a) Q = (%s.Q(s[a s/x]))";
    9.15 -by(Simp_tac 1);
    9.16 +by (Simp_tac 1);
    9.17  qed "swp_Ass";
    9.18  
    9.19  goalw Hoare.thy [swp_def] "swp (c;d) Q = swp c (swp d Q)";
    9.20 -by(Simp_tac 1);
    9.21 -br ext 1;
    9.22 +by (Simp_tac 1);
    9.23 +by (rtac ext 1);
    9.24  by (Fast_tac 1);
    9.25  qed "swp_Semi";
    9.26  
    9.27  goalw Hoare.thy [swp_def]
    9.28    "swp (IF b THEN c ELSE d) Q = (%s. (b s --> swp c Q s) & \
    9.29  \                                    (~b s --> swp d Q s))";
    9.30 -by(Simp_tac 1);
    9.31 -br ext 1;
    9.32 +by (Simp_tac 1);
    9.33 +by (rtac ext 1);
    9.34  by (Fast_tac 1);
    9.35  qed "swp_If";
    9.36  
    9.37  goalw Hoare.thy [swp_def]
    9.38    "!!s. b s ==> swp (WHILE b DO c) Q s = swp (c;WHILE b DO c) Q s";
    9.39 -by(stac C_While_If 1);
    9.40 -by(Asm_simp_tac 1);
    9.41 +by (stac C_While_If 1);
    9.42 +by (Asm_simp_tac 1);
    9.43  qed "swp_While_True";
    9.44  
    9.45  goalw Hoare.thy [swp_def] "!!s. ~b s ==> swp (WHILE b DO c) Q s = Q s";
    9.46 -by(stac C_While_If 1);
    9.47 -by(Asm_simp_tac 1);
    9.48 +by (stac C_While_If 1);
    9.49 +by (Asm_simp_tac 1);
    9.50  by (Fast_tac 1);
    9.51  qed "swp_While_False";
    9.52  
    9.53 @@ -73,12 +73,12 @@
    9.54  AddSIs [hoare.skip, hoare.ass, hoare.semi, hoare.If];
    9.55  
    9.56  goal Hoare.thy "!Q. |- {swp c Q} c {Q}";
    9.57 -by(com.induct_tac "c" 1);
    9.58 -by(ALLGOALS Simp_tac);
    9.59 +by (com.induct_tac "c" 1);
    9.60 +by (ALLGOALS Simp_tac);
    9.61  by (REPEAT_FIRST Fast_tac);
    9.62  by (deepen_tac (!claset addIs [hoare.conseq]) 0 1);
    9.63  by (Step_tac 1);
    9.64 -br hoare.conseq 1;
    9.65 +by (rtac hoare.conseq 1);
    9.66    be thin_rl 1;
    9.67    by (Fast_tac 1);
    9.68   br hoare.While 1;
    9.69 @@ -91,13 +91,13 @@
    9.70   by(safe_tac HOL_cs);
    9.71   by(rotate_tac ~1 1);
    9.72   by(Asm_full_simp_tac 1);
    9.73 -by(rotate_tac ~1 1);
    9.74 -by(Asm_full_simp_tac 1);
    9.75 +by (rotate_tac ~1 1);
    9.76 +by (Asm_full_simp_tac 1);
    9.77  qed_spec_mp "swp_is_pre";
    9.78  
    9.79  goal Hoare.thy "!!c. |= {P}c{Q} ==> |- {P}c{Q}";
    9.80 -br (swp_is_pre RSN (2,hoare.conseq)) 1;
    9.81 +by (rtac (swp_is_pre RSN (2,hoare.conseq)) 1);
    9.82   by (Fast_tac 2);
    9.83 -by(rewrite_goals_tac [hoare_valid_def,swp_def]);
    9.84 +by (rewrite_goals_tac [hoare_valid_def,swp_def]);
    9.85  by (Fast_tac 1);
    9.86  qed "hoare_relative_complete";
    10.1 --- a/src/HOL/IMP/Transition.ML	Thu Sep 26 11:11:22 1996 +0200
    10.2 +++ b/src/HOL/IMP/Transition.ML	Thu Sep 26 12:47:47 1996 +0200
    10.3 @@ -23,30 +23,30 @@
    10.4  AddIs evalc1.intrs;
    10.5  
    10.6  goal Transition.thy "!!s. (SKIP,s) -m-> (SKIP,t) ==> s = t & m = 0";
    10.7 -be rel_pow_E2 1;
    10.8 +by (etac rel_pow_E2 1);
    10.9  by (Asm_full_simp_tac 1);
   10.10 -by(Fast_tac 1);
   10.11 +by (Fast_tac 1);
   10.12  val hlemma = result();
   10.13  
   10.14  
   10.15  goal Transition.thy
   10.16    "!s t u c d. (c,s) -n-> (SKIP,t) --> (d,t) -*-> (SKIP,u) --> \
   10.17  \              (c;d, s) -*-> (SKIP, u)";
   10.18 -by(nat_ind_tac "n" 1);
   10.19 +by (nat_ind_tac "n" 1);
   10.20   (* case n = 0 *)
   10.21   by(fast_tac (!claset addIs [rtrancl_into_rtrancl2])1);
   10.22  (* induction step *)
   10.23  by (safe_tac (!claset addSDs [rel_pow_Suc_D2]));
   10.24 -by(split_all_tac 1);
   10.25 -by(fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
   10.26 +by (split_all_tac 1);
   10.27 +by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
   10.28  qed_spec_mp "lemma1";
   10.29  
   10.30  
   10.31  goal Transition.thy "!!c s s1. <c,s> -c-> s1 ==> (c,s) -*-> (SKIP,s1)";
   10.32 -be evalc.induct 1;
   10.33 +by (etac evalc.induct 1);
   10.34  
   10.35  (* SKIP *)
   10.36 -br rtrancl_refl 1;
   10.37 +by (rtac rtrancl_refl 1);
   10.38  
   10.39  (* ASSIGN *)
   10.40  by (fast_tac (!claset addSIs [r_into_rtrancl]) 1);
   10.41 @@ -69,7 +69,7 @@
   10.42  goal Transition.thy
   10.43    "!c d s u. (c;d,s) -n-> (SKIP,u) --> \
   10.44  \            (? t m. (c,s) -*-> (SKIP,t) & (d,t) -m-> (SKIP,u) & m <= n)";
   10.45 -by(nat_ind_tac "n" 1);
   10.46 +by (nat_ind_tac "n" 1);
   10.47   (* case n = 0 *)
   10.48   by (fast_tac (!claset addss !simpset) 1);
   10.49  (* induction step *)
   10.50 @@ -93,17 +93,17 @@
   10.51  by (fast_tac (!claset addSDs [lemma2,rel_pow_imp_rtrancl]) 1);
   10.52  
   10.53  (* IF *)
   10.54 -be rel_pow_E2 1;
   10.55 +by (etac rel_pow_E2 1);
   10.56  by (Asm_full_simp_tac 1);
   10.57  by (fast_tac (!claset addSDs [rel_pow_imp_rtrancl]) 1);
   10.58  
   10.59  (* WHILE, induction on the length of the computation *)
   10.60 -by(rotate_tac 1 1);
   10.61 +by (rotate_tac 1 1);
   10.62  by (etac rev_mp 1);
   10.63  by (res_inst_tac [("x","s")] spec 1);
   10.64 -by(res_inst_tac [("n","n")] less_induct 1);
   10.65 +by (res_inst_tac [("n","n")] less_induct 1);
   10.66  by (strip_tac 1);
   10.67 -be rel_pow_E2 1;
   10.68 +by (etac rel_pow_E2 1);
   10.69   by (Asm_full_simp_tac 1);
   10.70  by (eresolve_tac evalc1_Es 1);
   10.71  
   10.72 @@ -111,7 +111,7 @@
   10.73   by (fast_tac (!claset addSDs [hlemma]) 1);
   10.74  
   10.75  (* WhileTrue *)
   10.76 -by(fast_tac(!claset addSDs[lemma2,le_imp_less_or_eq,less_Suc_eq RS iffD2])1);
   10.77 +by (fast_tac(!claset addSDs[lemma2,le_imp_less_or_eq,less_Suc_eq RS iffD2])1);
   10.78  
   10.79  qed_spec_mp "evalc1_impl_evalc";
   10.80  
   10.81 @@ -128,17 +128,17 @@
   10.82  goal Transition.thy
   10.83   "!!c1. (c1,s1) -*-> (SKIP,s2) ==> \
   10.84  \ (c2,s2) -*-> cs3 --> (c1;c2,s1) -*-> cs3";
   10.85 -be converse_rtrancl_induct2 1;
   10.86 -by(fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
   10.87 -by(fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
   10.88 +by (etac converse_rtrancl_induct2 1);
   10.89 +by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
   10.90 +by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
   10.91  qed_spec_mp "my_lemma1";
   10.92  
   10.93  
   10.94  goal Transition.thy "!!c s s1. <c,s> -c-> s1 ==> (c,s) -*-> (SKIP,s1)";
   10.95 -be evalc.induct 1;
   10.96 +by (etac evalc.induct 1);
   10.97  
   10.98  (* SKIP *)
   10.99 -br rtrancl_refl 1;
  10.100 +by (rtac rtrancl_refl 1);
  10.101  
  10.102  (* ASSIGN *)
  10.103  by (fast_tac (!claset addSIs [r_into_rtrancl]) 1);
  10.104 @@ -193,15 +193,15 @@
  10.105  
  10.106  goal Transition.thy 
  10.107    "!!c s. ((c,s) -1-> (c',s')) ==> (!t. <c',s'> -c-> t --> <c,s> -c-> t)";
  10.108 -be evalc1.induct 1;
  10.109 +by (etac evalc1.induct 1);
  10.110  auto();
  10.111  qed_spec_mp "FB_lemma3";
  10.112  
  10.113  val [major] = goal Transition.thy
  10.114    "(c,s) -*-> (c',s') ==> <c',s'> -c-> t --> <c,s> -c-> t";
  10.115 -br (major RS rtrancl_induct2) 1;
  10.116 -by(Fast_tac 1);
  10.117 -by(fast_tac (!claset addIs [FB_lemma3] addbefore (split_all_tac 1)) 1);
  10.118 +by (rtac (major RS rtrancl_induct2) 1);
  10.119 +by (Fast_tac 1);
  10.120 +by (fast_tac (!claset addIs [FB_lemma3] addbefore (split_all_tac 1)) 1);
  10.121  qed_spec_mp "FB_lemma2";
  10.122  
  10.123  goal Transition.thy "!!c. (c,s) -*-> (SKIP,t) ==> <c,s> -c-> t";
    11.1 --- a/src/HOL/IMP/VC.ML	Thu Sep 26 11:11:22 1996 +0200
    11.2 +++ b/src/HOL/IMP/VC.ML	Thu Sep 26 12:47:47 1996 +0200
    11.3 @@ -13,7 +13,7 @@
    11.4  val lemma = prove_goal HOL.thy "!s.P s --> P s" (K[Fast_tac 1]);
    11.5  
    11.6  goal VC.thy "!Q. (!s. vc c Q s) --> |- {wp c Q} astrip c {Q}";
    11.7 -by(acom.induct_tac "c" 1);
    11.8 +by (acom.induct_tac "c" 1);
    11.9      by(ALLGOALS Simp_tac);
   11.10      by(Fast_tac 1);
   11.11     by(Fast_tac 1);
   11.12 @@ -21,7 +21,7 @@
   11.13   (* if *)
   11.14   by(Deepen_tac 4 1);
   11.15  (* while *)
   11.16 -by(safe_tac HOL_cs);
   11.17 +by (safe_tac HOL_cs);
   11.18  by (resolve_tac hoare.intrs 1);
   11.19    br lemma 1;
   11.20   brs hoare.intrs 1;
   11.21 @@ -30,19 +30,19 @@
   11.22  qed "vc_sound";
   11.23  
   11.24  goal VC.thy "!P Q. (!s. P s --> Q s) --> (!s. wp c P s --> wp c Q s)";
   11.25 -by(acom.induct_tac "c" 1);
   11.26 +by (acom.induct_tac "c" 1);
   11.27      by(ALLGOALS Asm_simp_tac);
   11.28 -by(EVERY1[rtac allI, rtac allI, rtac impI]);
   11.29 -by(EVERY1[etac allE, etac allE, etac mp]);
   11.30 -by(EVERY1[etac allE, etac allE, etac mp, atac]);
   11.31 +by (EVERY1[rtac allI, rtac allI, rtac impI]);
   11.32 +by (EVERY1[etac allE, etac allE, etac mp]);
   11.33 +by (EVERY1[etac allE, etac allE, etac mp, atac]);
   11.34  qed_spec_mp "wp_mono";
   11.35  
   11.36  goal VC.thy "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)";
   11.37 -by(acom.induct_tac "c" 1);
   11.38 +by (acom.induct_tac "c" 1);
   11.39      by(ALLGOALS Asm_simp_tac);
   11.40 -by(safe_tac HOL_cs);
   11.41 -by(EVERY[etac allE 1,etac allE 1,etac impE 1,etac allE 2,etac mp 2,atac 2]);
   11.42 -by(fast_tac (HOL_cs addEs [wp_mono]) 1);
   11.43 +by (safe_tac HOL_cs);
   11.44 +by (EVERY[etac allE 1,etac allE 1,etac impE 1,etac allE 2,etac mp 2,atac 2]);
   11.45 +by (fast_tac (HOL_cs addEs [wp_mono]) 1);
   11.46  qed_spec_mp "vc_mono";
   11.47  
   11.48  goal VC.thy
   11.49 @@ -64,12 +64,12 @@
   11.50   by(res_inst_tac [("x","Awhile b Pa ac")] exI 1);
   11.51   by(Asm_simp_tac 1);
   11.52  by (safe_tac HOL_cs);
   11.53 -by(res_inst_tac [("x","ac")] exI 1);
   11.54 -by(Asm_simp_tac 1);
   11.55 -by(fast_tac (HOL_cs addSEs [wp_mono,vc_mono]) 1);
   11.56 +by (res_inst_tac [("x","ac")] exI 1);
   11.57 +by (Asm_simp_tac 1);
   11.58 +by (fast_tac (HOL_cs addSEs [wp_mono,vc_mono]) 1);
   11.59  qed "vc_complete";
   11.60  
   11.61  goal VC.thy "!Q. vcwp c Q = (vc c Q, wp c Q)";
   11.62 -by(acom.induct_tac "c" 1);
   11.63 -by(ALLGOALS (asm_simp_tac (!simpset addsimps [Let_def])));
   11.64 +by (acom.induct_tac "c" 1);
   11.65 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [Let_def])));
   11.66  qed "vcwp_vc_wp";
    12.1 --- a/src/HOL/Lambda/Commutation.ML	Thu Sep 26 11:11:22 1996 +0200
    12.2 +++ b/src/HOL/Lambda/Commutation.ML	Thu Sep 26 12:47:47 1996 +0200
    12.3 @@ -11,30 +11,30 @@
    12.4  (*** square ***)
    12.5  
    12.6  goalw Commutation.thy [square_def] "!!R. square R S T U ==> square S R U T";
    12.7 -by(Fast_tac 1);
    12.8 +by (Fast_tac 1);
    12.9  qed "square_sym";
   12.10  
   12.11  goalw Commutation.thy [square_def]
   12.12    "!!R. [| square R S T U; T <= T' |] ==> square R S T' U";
   12.13 -by(Fast_tac 1);
   12.14 +by (Fast_tac 1);
   12.15  qed "square_subset";
   12.16  
   12.17  goalw Commutation.thy [square_def]
   12.18    "!!R. [| square R S T (R^=); S <= T |] ==> square (R^=) S T (R^=)";
   12.19 -by(Fast_tac 1);
   12.20 +by (Fast_tac 1);
   12.21  qed "square_reflcl";
   12.22  
   12.23  goalw Commutation.thy [square_def]
   12.24    "!!R. square R S S T ==> square (R^*) S S (T^*)";
   12.25 -by(strip_tac 1);
   12.26 +by (strip_tac 1);
   12.27  by (etac rtrancl_induct 1);
   12.28 -by(Fast_tac 1);
   12.29 -by(best_tac (!claset addSEs [rtrancl_into_rtrancl]) 1);
   12.30 +by (Fast_tac 1);
   12.31 +by (best_tac (!claset addSEs [rtrancl_into_rtrancl]) 1);
   12.32  qed "square_rtrancl";
   12.33  
   12.34  goalw Commutation.thy [commute_def]
   12.35   "!!R. square R S (S^*) (R^=) ==> commute (R^*) (S^*)";
   12.36 -by(fast_tac (!claset addDs [square_reflcl,square_sym RS square_rtrancl]
   12.37 +by (fast_tac (!claset addDs [square_reflcl,square_sym RS square_rtrancl]
   12.38                       addEs [r_into_rtrancl]
   12.39                       addss !simpset) 1);
   12.40  qed "square_rtrancl_reflcl_commute";
   12.41 @@ -42,23 +42,23 @@
   12.42  (*** commute ***)
   12.43  
   12.44  goalw Commutation.thy [commute_def] "!!R. commute R S ==> commute S R";
   12.45 -by(fast_tac (!claset addIs [square_sym]) 1);
   12.46 +by (fast_tac (!claset addIs [square_sym]) 1);
   12.47  qed "commute_sym";
   12.48  
   12.49  goalw Commutation.thy [commute_def] "!!R. commute R S ==> commute (R^*) (S^*)";
   12.50 -by(fast_tac (!claset addIs [square_rtrancl,square_sym]) 1);
   12.51 +by (fast_tac (!claset addIs [square_rtrancl,square_sym]) 1);
   12.52  qed "commute_rtrancl";
   12.53  
   12.54  goalw Commutation.thy [commute_def,square_def]
   12.55    "!!R. [| commute R T; commute S T |] ==> commute (R Un S) T";
   12.56 -by(Fast_tac 1);
   12.57 +by (Fast_tac 1);
   12.58  qed "commute_Un";
   12.59  
   12.60  (*** diamond, confluence and union ***)
   12.61  
   12.62  goalw Commutation.thy [diamond_def]
   12.63    "!!R. [| diamond R; diamond S; commute R S |] ==> diamond (R Un S)";
   12.64 -by(REPEAT(ares_tac [commute_Un,commute_sym] 1));
   12.65 +by (REPEAT(ares_tac [commute_Un,commute_sym] 1));
   12.66  qed "diamond_Un";
   12.67  
   12.68  goalw Commutation.thy [diamond_def] "!!R. diamond R ==> confluent (R)";
   12.69 @@ -67,20 +67,20 @@
   12.70  
   12.71  goalw Commutation.thy [diamond_def]
   12.72    "!!R. square R R (R^=) (R^=) ==> confluent R";
   12.73 -by(fast_tac (!claset addIs [square_rtrancl_reflcl_commute,r_into_rtrancl]
   12.74 +by (fast_tac (!claset addIs [square_rtrancl_reflcl_commute,r_into_rtrancl]
   12.75                         addEs [square_subset]) 1);
   12.76  qed "square_reflcl_confluent";
   12.77  
   12.78  goal Commutation.thy
   12.79   "!!R. [| confluent R; confluent S; commute (R^*) (S^*) |] \
   12.80  \      ==> confluent(R Un S)";
   12.81 -br (rtrancl_Un_rtrancl RS subst) 1;
   12.82 +by (rtac (rtrancl_Un_rtrancl RS subst) 1);
   12.83  by (fast_tac (!claset addDs [diamond_Un] addIs [diamond_confluent]) 1);
   12.84  qed "confluent_Un";
   12.85  
   12.86  goal Commutation.thy
   12.87    "!!R.[| diamond(R); T <= R; R <= T^* |] ==> confluent(T)";
   12.88 -by(fast_tac (!claset addIs [diamond_confluent]
   12.89 +by (fast_tac (!claset addIs [diamond_confluent]
   12.90                      addDs [rtrancl_subset RS sym] addss !simpset) 1);
   12.91  qed "diamond_to_confluence";
   12.92  
   12.93 @@ -92,9 +92,9 @@
   12.94   by(fast_tac (HOL_cs addIs
   12.95        [Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans,
   12.96         rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD])1);
   12.97 -by(safe_tac HOL_cs);
   12.98 +by (safe_tac HOL_cs);
   12.99  by (etac rtrancl_induct 1);
  12.100   by(Fast_tac 1);
  12.101 -by(slow_best_tac (!claset addIs [r_into_rtrancl]
  12.102 +by (slow_best_tac (!claset addIs [r_into_rtrancl]
  12.103                      addEs [rtrancl_trans,r_into_rtrancl RS rtrancl_trans]) 1);
  12.104  qed "Church_Rosser_confluent";
    13.1 --- a/src/HOL/Lambda/Eta.ML	Thu Sep 26 11:11:22 1996 +0200
    13.2 +++ b/src/HOL/Lambda/Eta.ML	Thu Sep 26 12:47:47 1996 +0200
    13.3 @@ -26,29 +26,29 @@
    13.4  section "Arithmetic lemmas";
    13.5  
    13.6  goal HOL.thy "!!P. P ==> P=True";
    13.7 -by(fast_tac HOL_cs 1);
    13.8 +by (fast_tac HOL_cs 1);
    13.9  qed "True_eq";
   13.10  
   13.11  Addsimps [less_not_sym RS True_eq];
   13.12  
   13.13  goal Arith.thy "i < j --> pred i < j";
   13.14 -by(nat_ind_tac "j" 1);
   13.15 -by(ALLGOALS(asm_simp_tac(!simpset addsimps [less_Suc_eq])));
   13.16 -by(nat_ind_tac "j1" 1);
   13.17 -by(ALLGOALS Asm_simp_tac);
   13.18 +by (nat_ind_tac "j" 1);
   13.19 +by (ALLGOALS(asm_simp_tac(!simpset addsimps [less_Suc_eq])));
   13.20 +by (nat_ind_tac "j1" 1);
   13.21 +by (ALLGOALS Asm_simp_tac);
   13.22  qed_spec_mp "less_imp_pred_less";
   13.23  
   13.24  goal Arith.thy "i<j --> ~ pred j < i";
   13.25 -by(nat_ind_tac "j" 1);
   13.26 -by(ALLGOALS(asm_simp_tac(!simpset addsimps [less_Suc_eq])));
   13.27 +by (nat_ind_tac "j" 1);
   13.28 +by (ALLGOALS(asm_simp_tac(!simpset addsimps [less_Suc_eq])));
   13.29  qed_spec_mp "less_imp_not_pred_less";
   13.30  Addsimps [less_imp_not_pred_less];
   13.31  
   13.32  goal Nat.thy "i < j --> j < Suc(Suc i) --> j = Suc i";
   13.33 -by(nat_ind_tac "j" 1);
   13.34 -by(ALLGOALS Simp_tac);
   13.35 -by(simp_tac(!simpset addsimps [less_Suc_eq])1);
   13.36 -by(fast_tac (HOL_cs addDs [less_not_sym]) 1);
   13.37 +by (nat_ind_tac "j" 1);
   13.38 +by (ALLGOALS Simp_tac);
   13.39 +by (simp_tac(!simpset addsimps [less_Suc_eq])1);
   13.40 +by (fast_tac (HOL_cs addDs [less_not_sym]) 1);
   13.41  qed_spec_mp "less_interval1";
   13.42  
   13.43  
   13.44 @@ -56,50 +56,50 @@
   13.45  
   13.46  goal Eta.thy "!i k. free (lift t k) i = \
   13.47  \                   (i < k & free t i | k < i & free t (pred i))";
   13.48 -by(db.induct_tac "t" 1);
   13.49 -by(ALLGOALS(asm_full_simp_tac (addsplit (!simpset) addcongs [conj_cong])));
   13.50 -by(fast_tac HOL_cs 2);
   13.51 -by(safe_tac (HOL_cs addSIs [iffI]));
   13.52 +by (db.induct_tac "t" 1);
   13.53 +by (ALLGOALS(asm_full_simp_tac (addsplit (!simpset) addcongs [conj_cong])));
   13.54 +by (fast_tac HOL_cs 2);
   13.55 +by (safe_tac (HOL_cs addSIs [iffI]));
   13.56  by (dtac Suc_mono 1);
   13.57 -by(ALLGOALS(Asm_full_simp_tac));
   13.58 -by(dtac less_trans_Suc 1 THEN atac 1);
   13.59 -by(dtac less_trans_Suc 2 THEN atac 2);
   13.60 -by(ALLGOALS(Asm_full_simp_tac));
   13.61 +by (ALLGOALS(Asm_full_simp_tac));
   13.62 +by (dtac less_trans_Suc 1 THEN atac 1);
   13.63 +by (dtac less_trans_Suc 2 THEN atac 2);
   13.64 +by (ALLGOALS(Asm_full_simp_tac));
   13.65  qed "free_lift";
   13.66  Addsimps [free_lift];
   13.67  
   13.68  goal Eta.thy "!i k t. free (s[t/k]) i = \
   13.69  \              (free s k & free t i | free s (if i<k then i else Suc i))";
   13.70 -by(db.induct_tac "s" 1);
   13.71 -by(ALLGOALS(asm_full_simp_tac (addsplit (!simpset) addsimps
   13.72 +by (db.induct_tac "s" 1);
   13.73 +by (ALLGOALS(asm_full_simp_tac (addsplit (!simpset) addsimps
   13.74  [less_not_refl2,less_not_refl2 RS not_sym])));
   13.75 -by(fast_tac HOL_cs 2);
   13.76 -by(safe_tac (HOL_cs addSIs [iffI]));
   13.77 -by(ALLGOALS(Asm_simp_tac));
   13.78 -by(fast_tac (HOL_cs addEs [less_imp_not_pred_less RS notE]) 1);
   13.79 -by(fast_tac (HOL_cs addDs [less_not_sym]) 1);
   13.80 +by (fast_tac HOL_cs 2);
   13.81 +by (safe_tac (HOL_cs addSIs [iffI]));
   13.82 +by (ALLGOALS(Asm_simp_tac));
   13.83 +by (fast_tac (HOL_cs addEs [less_imp_not_pred_less RS notE]) 1);
   13.84 +by (fast_tac (HOL_cs addDs [less_not_sym]) 1);
   13.85  by (dtac Suc_mono 1);
   13.86 -by(dtac less_interval1 1 THEN atac 1);
   13.87 -by(asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
   13.88 -by(dtac less_trans_Suc 1 THEN atac 1);
   13.89 -by(Asm_full_simp_tac 1);
   13.90 +by (dtac less_interval1 1 THEN atac 1);
   13.91 +by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
   13.92 +by (dtac less_trans_Suc 1 THEN atac 1);
   13.93 +by (Asm_full_simp_tac 1);
   13.94  qed "free_subst";
   13.95  Addsimps [free_subst];
   13.96  
   13.97  goal Eta.thy "!!s. s -e> t ==> !i. free t i = free s i";
   13.98  by (etac eta.induct 1);
   13.99 -by(ALLGOALS(asm_simp_tac (!simpset addsimps [decr_def] addcongs [conj_cong])));
  13.100 +by (ALLGOALS(asm_simp_tac (!simpset addsimps [decr_def] addcongs [conj_cong])));
  13.101  qed_spec_mp "free_eta";
  13.102  
  13.103  goal Eta.thy "!!s. [| s -e> t; ~free s i |] ==> ~free t i";
  13.104 -by(asm_simp_tac (!simpset addsimps [free_eta]) 1);
  13.105 +by (asm_simp_tac (!simpset addsimps [free_eta]) 1);
  13.106  qed "not_free_eta";
  13.107  
  13.108  goal Eta.thy "!i t u. ~free s i --> s[t/i] = s[u/i]";
  13.109 -by(db.induct_tac "s" 1);
  13.110 -by(ALLGOALS(simp_tac (addsplit (!simpset))));
  13.111 -by(fast_tac HOL_cs 1);
  13.112 -by(fast_tac HOL_cs 1);
  13.113 +by (db.induct_tac "s" 1);
  13.114 +by (ALLGOALS(simp_tac (addsplit (!simpset))));
  13.115 +by (fast_tac HOL_cs 1);
  13.116 +by (fast_tac HOL_cs 1);
  13.117  qed_spec_mp "subst_not_free";
  13.118  
  13.119  goalw Eta.thy [decr_def] "!!s. ~free s i ==> s[t/i] = decr s i";
  13.120 @@ -108,8 +108,8 @@
  13.121  
  13.122  goal Eta.thy "!!s. s -e> t ==> !u i. s[u/i] -e> t[u/i]";
  13.123  by (etac eta.induct 1);
  13.124 -by(ALLGOALS(asm_simp_tac (!simpset addsimps [subst_subst RS sym,decr_def])));
  13.125 -by(asm_simp_tac (!simpset addsimps [subst_decr]) 1);
  13.126 +by (ALLGOALS(asm_simp_tac (!simpset addsimps [subst_subst RS sym,decr_def])));
  13.127 +by (asm_simp_tac (!simpset addsimps [subst_decr]) 1);
  13.128  qed_spec_mp "eta_subst";
  13.129  Addsimps [eta_subst];
  13.130  
  13.131 @@ -122,11 +122,11 @@
  13.132  goalw Eta.thy [square_def,id_def]  "square eta eta (eta^=) (eta^=)";
  13.133  by (rtac (impI RS allI RS allI) 1);
  13.134  by (etac eta.induct 1);
  13.135 -by(ALLGOALS(fast_tac (!claset addSEs [eta_decr,not_free_eta] addss !simpset)));
  13.136 +by (ALLGOALS(fast_tac (!claset addSEs [eta_decr,not_free_eta] addss !simpset)));
  13.137  val lemma = result();
  13.138  
  13.139  goal Eta.thy "confluent(eta)";
  13.140 -by(rtac (lemma RS square_reflcl_confluent) 1);
  13.141 +by (rtac (lemma RS square_reflcl_confluent) 1);
  13.142  qed "eta_confluent";
  13.143  
  13.144  section "Congruence rules for -e>>";
  13.145 @@ -155,69 +155,69 @@
  13.146  
  13.147  goal Eta.thy "!!s t. s -> t ==> (!i. free t i --> free s i)";
  13.148  by (etac beta.induct 1);
  13.149 -by(ALLGOALS(Asm_full_simp_tac));
  13.150 +by (ALLGOALS(Asm_full_simp_tac));
  13.151  qed_spec_mp "free_beta";
  13.152  
  13.153  goalw Eta.thy [decr_def] "!!s t. s -> t ==> (!i. decr s i -> decr t i)";
  13.154  by (etac beta.induct 1);
  13.155 -by(ALLGOALS(asm_full_simp_tac (!simpset addsimps [subst_subst RS sym])));
  13.156 +by (ALLGOALS(asm_full_simp_tac (!simpset addsimps [subst_subst RS sym])));
  13.157  qed_spec_mp "beta_decr";
  13.158  
  13.159  goalw Eta.thy [decr_def]
  13.160    "decr (Var i) k = (if i<=k then Var i else Var(pred i))";
  13.161 -by(simp_tac (addsplit (!simpset) addsimps [le_def]) 1);
  13.162 +by (simp_tac (addsplit (!simpset) addsimps [le_def]) 1);
  13.163  qed "decr_Var";
  13.164  Addsimps [decr_Var];
  13.165  
  13.166  goalw Eta.thy [decr_def] "decr (s@t) i = (decr s i)@(decr t i)";
  13.167 -by(Simp_tac 1);
  13.168 +by (Simp_tac 1);
  13.169  qed "decr_App";
  13.170  Addsimps [decr_App];
  13.171  
  13.172  goalw Eta.thy [decr_def] "decr (Fun s) i = Fun (decr s (Suc i))";
  13.173 -by(Simp_tac 1);
  13.174 +by (Simp_tac 1);
  13.175  qed "decr_Fun";
  13.176  Addsimps [decr_Fun];
  13.177  
  13.178  goal Eta.thy "!i. ~free t (Suc i) --> decr t i = decr t (Suc i)";
  13.179 -by(db.induct_tac "t" 1);
  13.180 -by(ALLGOALS(asm_simp_tac (addsplit (!simpset) addsimps [le_def, less_Suc_eq])));
  13.181 -by(fast_tac HOL_cs 1);
  13.182 +by (db.induct_tac "t" 1);
  13.183 +by (ALLGOALS(asm_simp_tac (addsplit (!simpset) addsimps [le_def, less_Suc_eq])));
  13.184 +by (fast_tac HOL_cs 1);
  13.185  qed "decr_not_free";
  13.186  Addsimps [decr_not_free];
  13.187  
  13.188  goal Eta.thy "!!s t. s -e> t ==> (!i. lift s i -e> lift t i)";
  13.189  by (etac eta.induct 1);
  13.190 -by(ALLGOALS(asm_simp_tac (addsplit (!simpset) addsimps [decr_def])));
  13.191 -by(asm_simp_tac (addsplit (!simpset) addsimps [subst_decr]) 1);
  13.192 +by (ALLGOALS(asm_simp_tac (addsplit (!simpset) addsimps [decr_def])));
  13.193 +by (asm_simp_tac (addsplit (!simpset) addsimps [subst_decr]) 1);
  13.194  qed_spec_mp "eta_lift";
  13.195  Addsimps [eta_lift];
  13.196  
  13.197  goal Eta.thy "!s t i. s -e> t --> u[s/i] -e>> u[t/i]";
  13.198 -by(db.induct_tac "u" 1);
  13.199 -by(ALLGOALS(asm_simp_tac (addsplit (!simpset))));
  13.200 -by(fast_tac (!claset addIs [r_into_rtrancl]) 1);
  13.201 -by(fast_tac (!claset addSIs [rtrancl_eta_App]) 1);
  13.202 -by(fast_tac (!claset addSIs [rtrancl_eta_Fun,eta_lift]) 1);
  13.203 +by (db.induct_tac "u" 1);
  13.204 +by (ALLGOALS(asm_simp_tac (addsplit (!simpset))));
  13.205 +by (fast_tac (!claset addIs [r_into_rtrancl]) 1);
  13.206 +by (fast_tac (!claset addSIs [rtrancl_eta_App]) 1);
  13.207 +by (fast_tac (!claset addSIs [rtrancl_eta_Fun,eta_lift]) 1);
  13.208  qed_spec_mp "rtrancl_eta_subst";
  13.209  
  13.210  goalw Eta.thy [square_def] "square beta eta (eta^*) (beta^=)";
  13.211  by (rtac (impI RS allI RS allI) 1);
  13.212  by (etac beta.induct 1);
  13.213 -by(strip_tac 1);
  13.214 +by (strip_tac 1);
  13.215  by (eresolve_tac eta_cases 1);
  13.216  by (eresolve_tac eta_cases 1);
  13.217 -by(fast_tac (!claset addss (!simpset addsimps [subst_decr])) 1);
  13.218 -by(slow_tac (!claset addIs [r_into_rtrancl,eta_subst]) 1);
  13.219 -by(slow_tac (!claset addIs [rtrancl_eta_subst]) 1);
  13.220 -by(slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppL]) 1);
  13.221 -by(slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppR]) 1);
  13.222 -by(slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_Fun,free_beta,beta_decr]
  13.223 +by (fast_tac (!claset addss (!simpset addsimps [subst_decr])) 1);
  13.224 +by (slow_tac (!claset addIs [r_into_rtrancl,eta_subst]) 1);
  13.225 +by (slow_tac (!claset addIs [rtrancl_eta_subst]) 1);
  13.226 +by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppL]) 1);
  13.227 +by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppR]) 1);
  13.228 +by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_Fun,free_beta,beta_decr]
  13.229                    addss (!simpset addsimps[subst_decr,symmetric decr_def])) 1);
  13.230  qed "square_beta_eta";
  13.231  
  13.232  goal Eta.thy "confluent(beta Un eta)";
  13.233 -by(REPEAT(ares_tac [square_rtrancl_reflcl_commute,confluent_Un,
  13.234 +by (REPEAT(ares_tac [square_rtrancl_reflcl_commute,confluent_Un,
  13.235                      beta_confluent,eta_confluent,square_beta_eta] 1));
  13.236  qed "confluent_beta_eta";
  13.237  
  13.238 @@ -225,7 +225,7 @@
  13.239  section "Implicit definition of -e>: Fun(lift s 0 @ Var 0) -e> s";
  13.240  
  13.241  goal Eta.thy "!i. (~free s i) = (? t. s = lift t i)";
  13.242 -by(db.induct_tac "s" 1);
  13.243 +by (db.induct_tac "s" 1);
  13.244    by(simp_tac (!simpset setloop (split_tac [expand_if])) 1);
  13.245    by(SELECT_GOAL(safe_tac HOL_cs)1);
  13.246     by(res_inst_tac [("m","nat"),("n","i")] nat_less_cases 1);
  13.247 @@ -258,24 +258,24 @@
  13.248    by(Simp_tac 1);
  13.249    by(fast_tac HOL_cs 1);
  13.250   by(Simp_tac 1);
  13.251 -by(Asm_simp_tac 1);
  13.252 -be thin_rl 1;
  13.253 -br allI 1;
  13.254 -br iffI 1;
  13.255 +by (Asm_simp_tac 1);
  13.256 +by (etac thin_rl 1);
  13.257 +by (rtac allI 1);
  13.258 +by (rtac iffI 1);
  13.259   be exE 1;
  13.260   by(res_inst_tac [("x","Fun t")] exI 1);
  13.261   by(Asm_simp_tac 1);
  13.262 -be exE 1;
  13.263 -be rev_mp 1;
  13.264 -by(res_inst_tac [("db","t")] db_case_distinction 1);
  13.265 +by (etac exE 1);
  13.266 +by (etac rev_mp 1);
  13.267 +by (res_inst_tac [("db","t")] db_case_distinction 1);
  13.268    by(simp_tac (!simpset setloop (split_tac [expand_if])) 1);
  13.269   by(Simp_tac 1);
  13.270 -by(Simp_tac 1);
  13.271 -by(fast_tac HOL_cs 1);
  13.272 +by (Simp_tac 1);
  13.273 +by (fast_tac HOL_cs 1);
  13.274  qed_spec_mp "not_free_iff_lifted";
  13.275  
  13.276  goalw Eta.thy [decr_def]
  13.277   "(!s. (~free s 0) --> R(Fun(s @ Var 0))(decr s 0)) = \
  13.278  \ (!s. R(Fun(lift s 0 @ Var 0))(s))";
  13.279 -by(fast_tac (HOL_cs addss (!simpset addsimps [lemma,not_free_iff_lifted])) 1);
  13.280 +by (fast_tac (HOL_cs addss (!simpset addsimps [lemma,not_free_iff_lifted])) 1);
  13.281  qed "explicit_is_implicit";
    14.1 --- a/src/HOL/Lambda/Lambda.ML	Thu Sep 26 11:11:22 1996 +0200
    14.2 +++ b/src/HOL/Lambda/Lambda.ML	Thu Sep 26 12:47:47 1996 +0200
    14.3 @@ -14,22 +14,22 @@
    14.4  goal Nat.thy "!!i. [| i < Suc j; j < k |] ==> i < k";
    14.5  by (rtac le_less_trans 1);
    14.6  by (assume_tac 2);
    14.7 -by(asm_full_simp_tac (!simpset addsimps [le_def, less_Suc_eq]) 1);
    14.8 -by(fast_tac (HOL_cs addEs [less_asym,less_irrefl]) 1);
    14.9 +by (asm_full_simp_tac (!simpset addsimps [le_def, less_Suc_eq]) 1);
   14.10 +by (fast_tac (HOL_cs addEs [less_asym,less_irrefl]) 1);
   14.11  qed "lt_trans1";
   14.12  
   14.13  goal Nat.thy "!!i. [| i < j; j < Suc(k) |] ==> i < k";
   14.14  by (etac less_le_trans 1);
   14.15 -by(asm_full_simp_tac (!simpset addsimps [le_def, less_Suc_eq]) 1);
   14.16 -by(fast_tac (HOL_cs addEs [less_asym,less_irrefl]) 1);
   14.17 +by (asm_full_simp_tac (!simpset addsimps [le_def, less_Suc_eq]) 1);
   14.18 +by (fast_tac (HOL_cs addEs [less_asym,less_irrefl]) 1);
   14.19  qed "lt_trans2";
   14.20  
   14.21  val major::prems = goal Nat.thy
   14.22    "[| i < Suc j; i < j ==> P; i = j ==> P |] ==> P";
   14.23  by (rtac (major RS lessE) 1);
   14.24 -by(ALLGOALS Asm_full_simp_tac);
   14.25 -by(resolve_tac prems 1 THEN etac sym 1);
   14.26 -by(fast_tac (HOL_cs addIs prems) 1);
   14.27 +by (ALLGOALS Asm_full_simp_tac);
   14.28 +by (resolve_tac prems 1 THEN etac sym 1);
   14.29 +by (fast_tac (HOL_cs addIs prems) 1);
   14.30  qed "leqE";
   14.31  
   14.32  goal Arith.thy "!!i. Suc i < j ==> i < pred j ";
   14.33 @@ -101,9 +101,9 @@
   14.34  
   14.35  goal Lambda.thy
   14.36    "!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i";
   14.37 -by(db.induct_tac "t" 1);
   14.38 -by(ALLGOALS Asm_simp_tac);
   14.39 -by(strip_tac 1);
   14.40 +by (db.induct_tac "t" 1);
   14.41 +by (ALLGOALS Asm_simp_tac);
   14.42 +by (strip_tac 1);
   14.43  by (excluded_middle_tac "nat < i" 1);
   14.44  by ((forward_tac [lt_trans2] 2) THEN (assume_tac 2));
   14.45  by (ALLGOALS(asm_full_simp_tac (addsplit(!simpset) addsimps [less_SucI])));
   14.46 @@ -111,9 +111,9 @@
   14.47  
   14.48  goal Lambda.thy "!i j s. j < Suc i --> \
   14.49  \         lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]";
   14.50 -by(db.induct_tac "t" 1);
   14.51 -by(ALLGOALS(asm_simp_tac (!simpset addsimps [lift_lift])));
   14.52 -by(strip_tac 1);
   14.53 +by (db.induct_tac "t" 1);
   14.54 +by (ALLGOALS(asm_simp_tac (!simpset addsimps [lift_lift])));
   14.55 +by (strip_tac 1);
   14.56  by (excluded_middle_tac "nat < j" 1);
   14.57  by (Asm_full_simp_tac 1);
   14.58  by (eres_inst_tac [("j","nat")] leqE 1);
   14.59 @@ -130,9 +130,9 @@
   14.60  goal Lambda.thy
   14.61    "!i j s. i < Suc j -->\
   14.62  \         lift (t[s/j]) i = (lift t i) [lift s i / Suc j]";
   14.63 -by(db.induct_tac "t" 1);
   14.64 -by(ALLGOALS(asm_simp_tac (!simpset addsimps [lift_lift])));
   14.65 -by(strip_tac 1);
   14.66 +by (db.induct_tac "t" 1);
   14.67 +by (ALLGOALS(asm_simp_tac (!simpset addsimps [lift_lift])));
   14.68 +by (strip_tac 1);
   14.69  by (excluded_middle_tac "nat < j" 1);
   14.70  by (Asm_full_simp_tac 1);
   14.71  by (eres_inst_tac [("i","j")] leqE 1);
   14.72 @@ -141,26 +141,26 @@
   14.73                 (!simpset addsimps [less_SucI,gt_pred])));
   14.74  by (hyp_subst_tac 1);
   14.75  by (asm_full_simp_tac (!simpset addsimps [less_SucI]) 1);
   14.76 -by(split_tac [expand_if] 1);
   14.77 +by (split_tac [expand_if] 1);
   14.78  by (asm_full_simp_tac (!simpset addsimps [less_SucI]) 1);
   14.79  qed "lift_subst_lt";
   14.80  
   14.81  goal Lambda.thy "!k s. (lift t k)[s/k] = t";
   14.82 -by(db.induct_tac "t" 1);
   14.83 -by(ALLGOALS Asm_simp_tac);
   14.84 -by(split_tac [expand_if] 1);
   14.85 -by(ALLGOALS Asm_full_simp_tac);
   14.86 +by (db.induct_tac "t" 1);
   14.87 +by (ALLGOALS Asm_simp_tac);
   14.88 +by (split_tac [expand_if] 1);
   14.89 +by (ALLGOALS Asm_full_simp_tac);
   14.90  qed "subst_lift";
   14.91  Addsimps [subst_lift];
   14.92  
   14.93  
   14.94  goal Lambda.thy "!i j u v. i < Suc j --> \
   14.95  \ t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]";
   14.96 -by(db.induct_tac "t" 1);
   14.97 -by(ALLGOALS(asm_simp_tac(!simpset addsimps [lift_lift RS sym,lift_subst_lt])));
   14.98 -by(strip_tac 1);
   14.99 +by (db.induct_tac "t" 1);
  14.100 +by (ALLGOALS(asm_simp_tac(!simpset addsimps [lift_lift RS sym,lift_subst_lt])));
  14.101 +by (strip_tac 1);
  14.102  by (excluded_middle_tac "nat < Suc(Suc j)" 1);
  14.103 -by(Asm_full_simp_tac 1);
  14.104 +by (Asm_full_simp_tac 1);
  14.105  by (forward_tac [lessI RS less_trans] 1);
  14.106  by (etac leqE 1);
  14.107  by (asm_simp_tac (!simpset addsimps [lt_pred]) 2);
  14.108 @@ -182,24 +182,24 @@
  14.109  (*** Equivalence proof for optimized substitution ***)
  14.110  
  14.111  goal Lambda.thy "!k. liftn 0 t k = t";
  14.112 -by(db.induct_tac "t" 1);
  14.113 -by(ALLGOALS(asm_simp_tac(addsplit(!simpset))));
  14.114 +by (db.induct_tac "t" 1);
  14.115 +by (ALLGOALS(asm_simp_tac(addsplit(!simpset))));
  14.116  qed "liftn_0";
  14.117  Addsimps [liftn_0];
  14.118  
  14.119  goal Lambda.thy "!k. liftn (Suc n) t k = lift (liftn n t k) k";
  14.120 -by(db.induct_tac "t" 1);
  14.121 -by(ALLGOALS(asm_simp_tac(addsplit(!simpset))));
  14.122 -by(fast_tac (HOL_cs addDs [add_lessD1]) 1);
  14.123 +by (db.induct_tac "t" 1);
  14.124 +by (ALLGOALS(asm_simp_tac(addsplit(!simpset))));
  14.125 +by (fast_tac (HOL_cs addDs [add_lessD1]) 1);
  14.126  qed "liftn_lift";
  14.127  Addsimps [liftn_lift];
  14.128  
  14.129  goal Lambda.thy "!n. substn t s n = t[liftn n s 0 / n]";
  14.130 -by(db.induct_tac "t" 1);
  14.131 -by(ALLGOALS(asm_simp_tac(addsplit(!simpset))));
  14.132 +by (db.induct_tac "t" 1);
  14.133 +by (ALLGOALS(asm_simp_tac(addsplit(!simpset))));
  14.134  qed "substn_subst_n";
  14.135  Addsimps [substn_subst_n];
  14.136  
  14.137  goal Lambda.thy "substn t s 0 = t[s/0]";
  14.138 -by(Simp_tac 1);
  14.139 +by (Simp_tac 1);
  14.140  qed "substn_subst_0";
    15.1 --- a/src/HOL/Lambda/ParRed.ML	Thu Sep 26 11:11:22 1996 +0200
    15.2 +++ b/src/HOL/Lambda/ParRed.ML	Thu Sep 26 12:47:47 1996 +0200
    15.3 @@ -21,13 +21,13 @@
    15.4  (*** beta <= par_beta <= beta^* ***)
    15.5  
    15.6  goal ParRed.thy "(Var n => t) = (t = Var n)";
    15.7 -by(Fast_tac 1);
    15.8 +by (Fast_tac 1);
    15.9  qed "par_beta_varL";
   15.10  Addsimps [par_beta_varL];
   15.11  
   15.12  goal ParRed.thy "t => t";
   15.13 -by(db.induct_tac "t" 1);
   15.14 -by(ALLGOALS Asm_simp_tac);
   15.15 +by (db.induct_tac "t" 1);
   15.16 +by (ALLGOALS Asm_simp_tac);
   15.17  qed"par_beta_refl";
   15.18  Addsimps [par_beta_refl];
   15.19  (* AddSIs [par_beta_refl]; causes search to blow up *)
   15.20 @@ -50,21 +50,21 @@
   15.21  (*** => ***)
   15.22  
   15.23  goal ParRed.thy "!t' n. t => t' --> lift t n => lift t' n";
   15.24 -by(db.induct_tac "t" 1);
   15.25 -by(ALLGOALS(fast_tac (!claset addss (!simpset))));
   15.26 +by (db.induct_tac "t" 1);
   15.27 +by (ALLGOALS(fast_tac (!claset addss (!simpset))));
   15.28  qed_spec_mp "par_beta_lift";
   15.29  Addsimps [par_beta_lift];
   15.30  
   15.31  goal ParRed.thy
   15.32    "!s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]";
   15.33 -by(db.induct_tac "t" 1);
   15.34 +by (db.induct_tac "t" 1);
   15.35    by(asm_simp_tac (addsplit(!simpset)) 1);
   15.36   by(strip_tac 1);
   15.37   bes par_beta_cases 1;
   15.38    by(Asm_simp_tac 1);
   15.39   by(asm_simp_tac (!simpset addsimps [subst_subst RS sym]) 1);
   15.40   by(fast_tac (!claset addSIs [par_beta_lift] addss (!simpset)) 1);
   15.41 -by(fast_tac (!claset addss (!simpset)) 1);
   15.42 +by (fast_tac (!claset addss (!simpset)) 1);
   15.43  qed_spec_mp "par_beta_subst";
   15.44  
   15.45  (*** Confluence (directly) ***)
   15.46 @@ -72,14 +72,14 @@
   15.47  goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)";
   15.48  by (rtac (impI RS allI RS allI) 1);
   15.49  by (etac par_beta.induct 1);
   15.50 -by(ALLGOALS(fast_tac (!claset addSIs [par_beta_subst])));
   15.51 +by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst])));
   15.52  qed "diamond_par_beta";
   15.53  
   15.54  
   15.55  (*** cd ***)
   15.56  
   15.57  goal ParRed.thy "!t. s => t --> t => cd s";
   15.58 -by(db.induct_tac "s" 1);
   15.59 +by (db.induct_tac "s" 1);
   15.60    by(Simp_tac 1);
   15.61   be rev_mp 1;
   15.62   by(db.induct_tac "db1" 1);
   15.63 @@ -89,10 +89,10 @@
   15.64  (*** Confluence (via cd) ***)
   15.65  
   15.66  goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)";
   15.67 -by(fast_tac (HOL_cs addIs [par_beta_cd]) 1);
   15.68 +by (fast_tac (HOL_cs addIs [par_beta_cd]) 1);
   15.69  qed "diamond_par_beta2";
   15.70  
   15.71  goal ParRed.thy "confluent(beta)";
   15.72 -by(fast_tac (HOL_cs addIs [diamond_par_beta2,diamond_to_confluence,
   15.73 +by (fast_tac (HOL_cs addIs [diamond_par_beta2,diamond_to_confluence,
   15.74                             par_beta_subset_beta,beta_subset_par_beta]) 1);
   15.75  qed"beta_confluent";
    16.1 --- a/src/HOL/MiniML/I.ML	Thu Sep 26 11:11:22 1996 +0200
    16.2 +++ b/src/HOL/MiniML/I.ML	Thu Sep 26 12:47:47 1996 +0200
    16.3 @@ -116,11 +116,11 @@
    16.4  
    16.5  goal I.thy
    16.6    "I e [] m id_subst = Ok(s,t,n) --> W e [] m = Ok(s, $s t, n)";
    16.7 -by(cut_facts_tac [(read_instantiate[("x","id_subst")]
    16.8 +by (cut_facts_tac [(read_instantiate[("x","id_subst")]
    16.9   (read_instantiate[("x","[]")](thm RS spec)
   16.10    RS spec RS spec))] 1);
   16.11 -by(Full_simp_tac 1);
   16.12 -by(fast_tac HOL_cs 1);
   16.13 +by (Full_simp_tac 1);
   16.14 +by (fast_tac HOL_cs 1);
   16.15  qed;
   16.16  
   16.17  assuming that thm is the undischarged version of I_correct_wrt_W.
   16.18 @@ -149,23 +149,23 @@
   16.19   be exE 1;
   16.20   by(split_all_tac 1);
   16.21   by(Full_simp_tac 1);
   16.22 -by(Asm_simp_tac 1);
   16.23 -by(strip_tac 1);
   16.24 -be exE 1;
   16.25 -by(REPEAT(etac conjE 1));
   16.26 -by(split_all_tac 1);
   16.27 -by(Full_simp_tac 1);
   16.28 -bd lemma 1;
   16.29 +by (Asm_simp_tac 1);
   16.30 +by (strip_tac 1);
   16.31 +by (etac exE 1);
   16.32 +by (REPEAT(etac conjE 1));
   16.33 +by (split_all_tac 1);
   16.34 +by (Full_simp_tac 1);
   16.35 +by (dtac lemma 1);
   16.36   by(fast_tac HOL_cs 1);
   16.37 -be exE 1;
   16.38 -be conjE 1;
   16.39 -by(hyp_subst_tac 1);
   16.40 -by(Asm_simp_tac 1);
   16.41 -br exI 1;
   16.42 -br conjI 1;
   16.43 +by (etac exE 1);
   16.44 +by (etac conjE 1);
   16.45 +by (hyp_subst_tac 1);
   16.46 +by (Asm_simp_tac 1);
   16.47 +by (rtac exI 1);
   16.48 +by (rtac conjI 1);
   16.49   br refl 1;
   16.50 -by(Simp_tac 1);
   16.51 -be disjE 1;
   16.52 +by (Simp_tac 1);
   16.53 +by (etac disjE 1);
   16.54   br disjI1 1;
   16.55   by(full_simp_tac (!simpset addsimps [o_def,subst_comp_tel]) 1);
   16.56   by(EVERY[etac allE 1, etac allE 1, etac allE 1,
   16.57 @@ -175,23 +175,23 @@
   16.58   br new_tv_subst_comp_2 1;
   16.59    by(fast_tac (HOL_cs addIs [W_var_ge RS new_tv_subst_le]) 1);
   16.60   by(fast_tac (HOL_cs addSIs [new_tv_subst_tel]addIs[new_tv_W RS conjunct1])1);
   16.61 -br disjI2 1;
   16.62 -be exE 1;
   16.63 -by(split_all_tac 1);
   16.64 -be conjE 1;
   16.65 -by(Full_simp_tac 1);
   16.66 -bd lemma 1;
   16.67 +by (rtac disjI2 1);
   16.68 +by (etac exE 1);
   16.69 +by (split_all_tac 1);
   16.70 +by (etac conjE 1);
   16.71 +by (Full_simp_tac 1);
   16.72 +by (dtac lemma 1);
   16.73   br conjI 1;
   16.74    by(fast_tac (HOL_cs addIs [W_var_ge RS new_tv_list_le]) 1);
   16.75   br new_tv_subst_comp_1 1;
   16.76     by(fast_tac (HOL_cs addIs [W_var_ge RS new_tv_subst_le]) 1);
   16.77   by(fast_tac (HOL_cs addSIs [new_tv_subst_tel]addIs[new_tv_W RS conjunct1])1);
   16.78 -be exE 1;
   16.79 -be conjE 1;
   16.80 -by(hyp_subst_tac 1);
   16.81 -by(asm_full_simp_tac (!simpset addsimps
   16.82 +by (etac exE 1);
   16.83 +by (etac conjE 1);
   16.84 +by (hyp_subst_tac 1);
   16.85 +by (asm_full_simp_tac (!simpset addsimps
   16.86       [o_def,subst_comp_te RS sym,subst_comp_tel RS sym]) 1);
   16.87 -by(asm_simp_tac (!simpset addcongs [conj_cong] addsimps
   16.88 +by (asm_simp_tac (!simpset addcongs [conj_cong] addsimps
   16.89             [eq_sym_conv,subst_comp_te RS sym,subst_comp_tel RS sym]) 1);
   16.90  qed_spec_mp "I_complete_wrt_W";
   16.91  
    17.1 --- a/src/HOL/MiniML/Maybe.ML	Thu Sep 26 11:11:22 1996 +0200
    17.2 +++ b/src/HOL/MiniML/Maybe.ML	Thu Sep 26 12:47:47 1996 +0200
    17.3 @@ -21,8 +21,8 @@
    17.4  
    17.5  goal Maybe.thy
    17.6    "((m bind f) = Fail) = ((m=Fail) | (? p. m = Ok p & f p = Fail))";
    17.7 -by(simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
    17.8 -by(fast_tac HOL_cs 1);
    17.9 +by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
   17.10 +by (fast_tac HOL_cs 1);
   17.11  qed "bind_eq_Fail";
   17.12  
   17.13  Addsimps [bind_eq_Fail];
    18.1 --- a/src/HOL/MiniML/MiniML.ML	Thu Sep 26 11:11:22 1996 +0200
    18.2 +++ b/src/HOL/MiniML/MiniML.ML	Thu Sep 26 12:47:47 1996 +0200
    18.3 @@ -16,7 +16,7 @@
    18.4  (* case VarI *)
    18.5  by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1);
    18.6  by (forw_inst_tac [("f1","$ s")] (nth_map RS sym) 1);
    18.7 -by( fast_tac (HOL_cs addIs [has_type.VarI] addss (!simpset delsimps [nth_map])) 1);
    18.8 +by ( fast_tac (HOL_cs addIs [has_type.VarI] addss (!simpset delsimps [nth_map])) 1);
    18.9  (* case AbsI *)
   18.10  by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1);
   18.11  (* case AppI *)
    19.1 --- a/src/HOL/MiniML/ROOT.ML	Thu Sep 26 11:11:22 1996 +0200
    19.2 +++ b/src/HOL/MiniML/ROOT.ML	Thu Sep 26 12:47:47 1996 +0200
    19.3 @@ -1,12 +1,12 @@
    19.4 -(*  Title: 	HOL/MiniML/ROOT.ML
    19.5 +(*  Title:      HOL/MiniML/ROOT.ML
    19.6      ID:         $Id$
    19.7 -    Author: 	Tobias Nipkow
    19.8 +    Author:     Tobias Nipkow
    19.9      Copyright   1995 TUM
   19.10  
   19.11  Type inference for let-free MiniML
   19.12  *)
   19.13  
   19.14 -HOL_build_completed;	(*Make examples fail if HOL did*)
   19.15 +HOL_build_completed;    (*Make examples fail if HOL did*)
   19.16  
   19.17  writeln"Root file for HOL/MiniML";
   19.18  Unify.trace_bound := 20;
    20.1 --- a/src/HOL/MiniML/Type.ML	Thu Sep 26 11:11:22 1996 +0200
    20.2 +++ b/src/HOL/MiniML/Type.ML	Thu Sep 26 12:47:47 1996 +0200
    20.3 @@ -6,7 +6,7 @@
    20.4  goalw thy [new_tv_def] 
    20.5        "!! n. [|mgu t1 t2 = Ok u; new_tv n t1; new_tv n t2|] ==> \
    20.6  \            new_tv n u";
    20.7 -by( fast_tac (set_cs addDs [mgu_free]) 1);
    20.8 +by ( fast_tac (set_cs addDs [mgu_free]) 1);
    20.9  qed "mgu_new";
   20.10  
   20.11  (* application of id_subst does not change type expression *)
   20.12 @@ -28,8 +28,8 @@
   20.13  Addsimps [app_subst_id_tel];
   20.14  
   20.15  goalw Type.thy [id_subst_def,o_def] "$s o id_subst = s";
   20.16 -br ext 1;
   20.17 -by(Simp_tac 1);
   20.18 +by (rtac ext 1);
   20.19 +by (Simp_tac 1);
   20.20  qed "o_id_subst";
   20.21  Addsimps[o_id_subst];
   20.22  
   20.23 @@ -117,36 +117,36 @@
   20.24  
   20.25  goalw Type.thy [id_subst_def,new_tv_def,free_tv_subst,dom_def,cod_def]
   20.26    "new_tv n id_subst";
   20.27 -by(Simp_tac 1);
   20.28 +by (Simp_tac 1);
   20.29  qed "new_tv_id_subst";
   20.30  Addsimps[new_tv_id_subst];
   20.31  
   20.32  goalw thy [new_tv_def]
   20.33    "new_tv n s = ((!m. n <= m --> (s m = TVar m)) & \
   20.34  \                (! l. l < n --> new_tv n (s l) ))";
   20.35 -by( safe_tac HOL_cs );
   20.36 +by ( safe_tac HOL_cs );
   20.37  (* ==> *)
   20.38 -by( fast_tac (HOL_cs addDs [leD] addss (!simpset addsimps [free_tv_subst,dom_def])) 1);
   20.39 -by( subgoal_tac "m:cod s | s l = TVar l" 1);
   20.40 -by( safe_tac HOL_cs );
   20.41 -by(fast_tac (HOL_cs addDs [UnI2] addss (!simpset addsimps [free_tv_subst])) 1);
   20.42 -by(dres_inst_tac [("P","%x. m:free_tv x")] subst 1 THEN atac 1);
   20.43 -by(Asm_full_simp_tac 1);
   20.44 -by(fast_tac (set_cs addss (!simpset addsimps [free_tv_subst,cod_def,dom_def])) 1);
   20.45 +by ( fast_tac (HOL_cs addDs [leD] addss (!simpset addsimps [free_tv_subst,dom_def])) 1);
   20.46 +by ( subgoal_tac "m:cod s | s l = TVar l" 1);
   20.47 +by ( safe_tac HOL_cs );
   20.48 +by (fast_tac (HOL_cs addDs [UnI2] addss (!simpset addsimps [free_tv_subst])) 1);
   20.49 +by (dres_inst_tac [("P","%x. m:free_tv x")] subst 1 THEN atac 1);
   20.50 +by (Asm_full_simp_tac 1);
   20.51 +by (fast_tac (set_cs addss (!simpset addsimps [free_tv_subst,cod_def,dom_def])) 1);
   20.52  (* <== *)
   20.53 -by( rewrite_goals_tac [free_tv_subst,cod_def,dom_def] );
   20.54 -by( safe_tac set_cs );
   20.55 -by( cut_inst_tac [("m","m"),("n","n")] less_linear 1);
   20.56 -by( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
   20.57 -by( cut_inst_tac [("m","ma"),("n","n")] less_linear 1);
   20.58 -by( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
   20.59 +by ( rewrite_goals_tac [free_tv_subst,cod_def,dom_def] );
   20.60 +by ( safe_tac set_cs );
   20.61 +by ( cut_inst_tac [("m","m"),("n","n")] less_linear 1);
   20.62 +by ( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
   20.63 +by ( cut_inst_tac [("m","ma"),("n","n")] less_linear 1);
   20.64 +by ( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
   20.65  qed "new_tv_subst";
   20.66  
   20.67  goal thy 
   20.68    "new_tv n  = list_all (new_tv n)";
   20.69  by (rtac ext 1);
   20.70 -by(list.induct_tac "x" 1);
   20.71 -by(ALLGOALS Asm_simp_tac);
   20.72 +by (list.induct_tac "x" 1);
   20.73 +by (ALLGOALS Asm_simp_tac);
   20.74  qed "new_tv_list";
   20.75  
   20.76  (* substitution affects only variables occurring freely *)
   20.77 @@ -169,7 +169,7 @@
   20.78    "n<=m --> new_tv n (t::typ) --> new_tv m t";
   20.79  by (typ.induct_tac "t" 1);
   20.80  (* case TVar n *)
   20.81 -by( fast_tac (HOL_cs addIs [less_le_trans] addss !simpset) 1);
   20.82 +by ( fast_tac (HOL_cs addIs [less_le_trans] addss !simpset) 1);
   20.83  (* case Fun t1 t2 *)
   20.84  by (Asm_simp_tac 1);
   20.85  qed_spec_mp "new_tv_le";
   20.86 @@ -177,9 +177,9 @@
   20.87  
   20.88  goal thy 
   20.89    "n<=m --> new_tv n (ts::typ list) --> new_tv m ts";
   20.90 -by( list.induct_tac "ts" 1);
   20.91 +by ( list.induct_tac "ts" 1);
   20.92  (* case [] *)
   20.93 -by(Simp_tac 1);
   20.94 +by (Simp_tac 1);
   20.95  (* case a#al *)
   20.96  by (fast_tac (HOL_cs addIs [new_tv_le] addss !simpset) 1);
   20.97  qed_spec_mp "new_tv_list_le";
   20.98 @@ -212,7 +212,7 @@
   20.99  
  20.100  goal thy
  20.101    "new_tv n s --> new_tv n (ts::typ list) --> new_tv n ($ s ts)";
  20.102 -by( simp_tac (!simpset addsimps [new_tv_list]) 1);
  20.103 +by ( simp_tac (!simpset addsimps [new_tv_list]) 1);
  20.104  by (list.induct_tac "ts" 1);
  20.105  by (ALLGOALS(fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst]))));
  20.106  qed_spec_mp "new_tv_subst_tel";
  20.107 @@ -221,7 +221,7 @@
  20.108  (* auxilliary lemma *)
  20.109  goal thy
  20.110    "new_tv n ts --> new_tv (Suc n) ((TVar n)#ts)";
  20.111 -by( simp_tac (!simpset addsimps [new_tv_list]) 1);
  20.112 +by ( simp_tac (!simpset addsimps [new_tv_list]) 1);
  20.113  by (list.induct_tac "ts" 1);
  20.114  by (ALLGOALS Asm_full_simp_tac);
  20.115  qed "new_tv_Suc_list";
  20.116 @@ -302,50 +302,50 @@
  20.117  (* some useful theorems *)
  20.118  goalw thy [free_tv_subst] 
  20.119        "!!v. v : cod s ==> v : free_tv s";
  20.120 -by( fast_tac set_cs 1);
  20.121 +by ( fast_tac set_cs 1);
  20.122  qed "codD";
  20.123   
  20.124  goalw thy [free_tv_subst,dom_def] 
  20.125        "!! x. x ~: free_tv s ==> s x = TVar x";
  20.126 -by( fast_tac set_cs 1);
  20.127 +by ( fast_tac set_cs 1);
  20.128  qed "not_free_impl_id";
  20.129  
  20.130  goalw thy [new_tv_def] 
  20.131        "!! n. [| new_tv n t; m:free_tv t |] ==> m<n";
  20.132 -by( fast_tac HOL_cs 1 );
  20.133 +by ( fast_tac HOL_cs 1 );
  20.134  qed "free_tv_le_new_tv";
  20.135  
  20.136  goal thy 
  20.137       "free_tv (s (v::nat)) <= cod s Un {v}";
  20.138 -by( cut_inst_tac [("P","v:dom s")] excluded_middle 1);
  20.139 -by( safe_tac (HOL_cs addSIs [subsetI]) );
  20.140 +by ( cut_inst_tac [("P","v:dom s")] excluded_middle 1);
  20.141 +by ( safe_tac (HOL_cs addSIs [subsetI]) );
  20.142  by (fast_tac (set_cs addss (!simpset addsimps [dom_def])) 1);
  20.143  by (fast_tac (set_cs addss (!simpset addsimps [cod_def])) 1);
  20.144  qed "free_tv_subst_var";
  20.145  
  20.146  goal thy 
  20.147       "free_tv ($ s (t::typ)) <= cod s Un free_tv t";
  20.148 -by( typ.induct_tac "t" 1);
  20.149 +by ( typ.induct_tac "t" 1);
  20.150  (* case TVar n *)
  20.151 -by( simp_tac (!simpset addsimps [free_tv_subst_var]) 1);
  20.152 +by ( simp_tac (!simpset addsimps [free_tv_subst_var]) 1);
  20.153  (* case Fun t1 t2 *)
  20.154 -by( fast_tac (set_cs addss !simpset) 1);
  20.155 +by ( fast_tac (set_cs addss !simpset) 1);
  20.156  qed "free_tv_app_subst_te";     
  20.157  
  20.158  goal thy 
  20.159       "free_tv ($ s (ts::typ list)) <= cod s Un free_tv ts";
  20.160 -by( list.induct_tac "ts" 1);
  20.161 +by ( list.induct_tac "ts" 1);
  20.162  (* case [] *)
  20.163  by (Simp_tac 1);
  20.164  (* case a#al *)
  20.165 -by( cut_facts_tac [free_tv_app_subst_te] 1);
  20.166 -by( fast_tac (set_cs addss !simpset) 1);
  20.167 +by ( cut_facts_tac [free_tv_app_subst_te] 1);
  20.168 +by ( fast_tac (set_cs addss !simpset) 1);
  20.169  qed "free_tv_app_subst_tel";
  20.170  
  20.171  goalw thy [free_tv_subst,dom_def]
  20.172       "free_tv (%u::nat. $ s1 (s2 u) :: typ) <=   \
  20.173  \     free_tv s1 Un free_tv s2";
  20.174 -by( fast_tac (set_cs addSDs [free_tv_app_subst_te RS
  20.175 +by ( fast_tac (set_cs addSDs [free_tv_app_subst_te RS
  20.176  subsetD,free_tv_subst_var RS subsetD] addss (
  20.177  !simpset addsimps [cod_def,dom_def])) 1);
  20.178  qed "free_tv_comp_subst";
    21.1 --- a/src/HOL/MiniML/W.ML	Thu Sep 26 11:11:22 1996 +0200
    21.2 +++ b/src/HOL/MiniML/W.ML	Thu Sep 26 12:47:47 1996 +0200
    21.3 @@ -22,11 +22,11 @@
    21.4                          setloop (split_tac [expand_bind])) 1);
    21.5  by (strip_tac 1);
    21.6  by (eres_inst_tac [("x","TVar(n) # a")] allE 1);
    21.7 -by( fast_tac (HOL_cs addss (!simpset addsimps [eq_sym_conv])) 1);
    21.8 +by ( fast_tac (HOL_cs addss (!simpset addsimps [eq_sym_conv])) 1);
    21.9  (* case App e1 e2 *)
   21.10  by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
   21.11  by (strip_tac 1);
   21.12 -by( rename_tac "sa ta na sb tb nb sc" 1);
   21.13 +by ( rename_tac "sa ta na sb tb nb sc" 1);
   21.14  by (res_inst_tac [("t2.0","$ sc tb")] has_type.AppI 1);
   21.15  by (res_inst_tac [("s1","sc")] (app_subst_TVar RS subst) 1);
   21.16  by (rtac (app_subst_Fun RS subst) 1);
   21.17 @@ -83,7 +83,7 @@
   21.18  
   21.19  (* auxiliary lemma *)
   21.20  goal Maybe.thy "(y = Ok x) = (Ok x = y)";
   21.21 -by( simp_tac (!simpset addsimps [eq_sym_conv]) 1);
   21.22 +by ( simp_tac (!simpset addsimps [eq_sym_conv]) 1);
   21.23  qed "rotate_Ok";
   21.24  
   21.25  
   21.26 @@ -121,7 +121,7 @@
   21.27  by (eres_inst_tac [("x","sa")] allE 1);
   21.28  by (eres_inst_tac [("x","ta")] allE 1);
   21.29  by (eres_inst_tac [("x","nb")] allE 1);
   21.30 -by( asm_full_simp_tac (!simpset addsimps [o_def,rotate_Ok]) 1);
   21.31 +by ( asm_full_simp_tac (!simpset addsimps [o_def,rotate_Ok]) 1);
   21.32  by (rtac conjI 1);
   21.33  by (rtac new_tv_subst_comp_2 1);
   21.34  by (rtac new_tv_subst_comp_2 1);
   21.35 @@ -134,25 +134,25 @@
   21.36      1);
   21.37  by (etac (sym RS mgu_new) 1);
   21.38  by (best_tac (HOL_cs addDs [W_var_geD] 
   21.39 -	             addIs [new_tv_subst_te,new_tv_list_le,
   21.40 -			    new_tv_subst_tel,
   21.41 -			    lessI RS less_imp_le RS new_tv_le,
   21.42 -			    lessI RS less_imp_le RS new_tv_subst_le,
   21.43 -			    new_tv_le]) 1);
   21.44 +                     addIs [new_tv_subst_te,new_tv_list_le,
   21.45 +                            new_tv_subst_tel,
   21.46 +                            lessI RS less_imp_le RS new_tv_le,
   21.47 +                            lessI RS less_imp_le RS new_tv_subst_le,
   21.48 +                            new_tv_le]) 1);
   21.49  by (fast_tac (HOL_cs addDs [W_var_geD] 
   21.50 -	             addIs [new_tv_list_le,new_tv_subst_tel,new_tv_le] 
   21.51 -		     addss (!simpset)) 1);
   21.52 +                     addIs [new_tv_list_le,new_tv_subst_tel,new_tv_le] 
   21.53 +                     addss (!simpset)) 1);
   21.54  by (rtac (lessI RS new_tv_subst_var) 1);
   21.55  by (etac (sym RS mgu_new) 1);
   21.56  by (best_tac (HOL_cs addSIs [lessI RS less_imp_le RS new_tv_le,new_tv_subst_te]
   21.57                       addDs [W_var_geD]
   21.58 -		     addIs [new_tv_list_le,
   21.59 -			    new_tv_subst_tel,
   21.60 -			    lessI RS less_imp_le RS new_tv_subst_le,
   21.61 -			    new_tv_le] 
   21.62 -		     addss !simpset) 1);
   21.63 +                     addIs [new_tv_list_le,
   21.64 +                            new_tv_subst_tel,
   21.65 +                            lessI RS less_imp_le RS new_tv_subst_le,
   21.66 +                            new_tv_le] 
   21.67 +                     addss !simpset) 1);
   21.68  by (fast_tac (HOL_cs addDs [W_var_geD] 
   21.69 -	             addIs [new_tv_list_le,new_tv_subst_tel,new_tv_le]
   21.70 +                     addIs [new_tv_list_le,new_tv_subst_tel,new_tv_le]
   21.71                       addss (!simpset)) 1);
   21.72  qed_spec_mp "new_tv_W";
   21.73  
   21.74 @@ -226,7 +226,7 @@
   21.75  (* case Var n *)
   21.76  by (strip_tac 1);
   21.77  by (simp_tac (!simpset addcongs [conj_cong] 
   21.78 -	      setloop (split_tac [expand_if])) 1);
   21.79 +              setloop (split_tac [expand_if])) 1);
   21.80  by (eresolve_tac has_type_casesE 1); 
   21.81  by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv,app_subst_list]) 1);
   21.82  by (res_inst_tac [("x","id_subst")] exI 1);
   21.83 @@ -243,7 +243,7 @@
   21.84  by (eres_inst_tac [("x","t2")] allE 1);
   21.85  by (eres_inst_tac [("x","Suc n")] allE 1);
   21.86  by (fast_tac (HOL_cs addss (!simpset addcongs [conj_cong]
   21.87 -			    setloop (split_tac [expand_bind]))) 1);
   21.88 +                            setloop (split_tac [expand_bind]))) 1);
   21.89  
   21.90  (* case App e1 e2 *)
   21.91  by (strip_tac 1);
   21.92 @@ -264,7 +264,7 @@
   21.93  by (safe_tac HOL_cs);
   21.94  by (fast_tac HOL_cs 1);
   21.95  by (fast_tac (HOL_cs addIs [sym RS W_var_geD,new_tv_W RS
   21.96 -			    conjunct1,new_tv_list_le,new_tv_subst_tel]) 1);
   21.97 +                            conjunct1,new_tv_list_le,new_tv_subst_tel]) 1);
   21.98  
   21.99  by (subgoal_tac
  21.100    "$ (%x.if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \
  21.101 @@ -279,11 +279,11 @@
  21.102  by (strip_tac 2);
  21.103  by (subgoal_tac "na ~=ma" 2);
  21.104  by (fast_tac (HOL_cs addDs [new_tv_W,sym RS W_var_geD,
  21.105 -			    new_tv_not_free_tv,new_tv_le]) 3);
  21.106 +                            new_tv_not_free_tv,new_tv_le]) 3);
  21.107  by (case_tac "na:free_tv sa" 2);
  21.108  (* na ~: free_tv sa *)
  21.109  by (asm_simp_tac (!simpset addsimps [not_free_impl_id]
  21.110 -		  setloop (split_tac [expand_if])) 3);
  21.111 +                  setloop (split_tac [expand_if])) 3);
  21.112  (* na : free_tv sa *)
  21.113  by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
  21.114  by (dtac eq_subst_tel_eq_free 2);
  21.115 @@ -292,7 +292,7 @@
  21.116  by (case_tac "na:dom sa" 2);
  21.117  (* na ~: dom sa *)
  21.118  by (asm_full_simp_tac (!simpset addsimps [dom_def] 
  21.119 -		       setloop (split_tac [expand_if])) 3);
  21.120 +                       setloop (split_tac [expand_if])) 3);
  21.121  (* na : dom sa *)
  21.122  by (rtac eq_free_eq_subst_te 2);
  21.123  by (strip_tac 2);
  21.124 @@ -302,9 +302,9 @@
  21.125  by (dtac new_tv_subst_tel 3);
  21.126  by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 3);
  21.127  by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss 
  21.128 -	      (!simpset addsimps [cod_def,free_tv_subst])) 3);
  21.129 +              (!simpset addsimps [cod_def,free_tv_subst])) 3);
  21.130  by (fast_tac (set_cs addss (!simpset addsimps [cod_def,free_tv_subst] 
  21.131 -			    setloop (split_tac [expand_if]))) 2);
  21.132 +                            setloop (split_tac [expand_if]))) 2);
  21.133  
  21.134  by (Simp_tac 2);  
  21.135  by (rtac eq_free_eq_subst_te 2);
  21.136 @@ -316,9 +316,9 @@
  21.137  by (fast_tac (HOL_cs addDs [new_tv_list_le,new_tv_subst_tel,new_tv_W,new_tv_not_free_tv]) 3);
  21.138  by (case_tac "na: free_tv t - free_tv sa" 2);
  21.139  (* case na ~: free_tv t - free_tv sa *)
  21.140 -by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
  21.141 +by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
  21.142  (* case na : free_tv t - free_tv sa *)
  21.143 -by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
  21.144 +by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
  21.145  by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
  21.146  by (dtac eq_subst_tel_eq_free 2);
  21.147  by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
  21.148 @@ -327,7 +327,7 @@
  21.149  by (asm_simp_tac (!simpset setloop (split_tac [expand_bind])) 1); 
  21.150  by (safe_tac HOL_cs );
  21.151  by (dtac mgu_Ok 1);
  21.152 -by( fast_tac (HOL_cs addss !simpset) 1);
  21.153 +by ( fast_tac (HOL_cs addss !simpset) 1);
  21.154  by (REPEAT (resolve_tac [exI,conjI] 1));
  21.155  by (fast_tac HOL_cs 1);
  21.156  by (fast_tac HOL_cs 1);
  21.157 @@ -336,13 +336,13 @@
  21.158  by (res_inst_tac [("x","rb")] exI 1);
  21.159  by (rtac conjI 1);
  21.160  by (dres_inst_tac [("x","ma")] fun_cong 2);
  21.161 -by( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2);
  21.162 +by ( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2);
  21.163  by (simp_tac (!simpset addsimps [subst_comp_tel RS sym]) 1);
  21.164  by (res_inst_tac [("ts2","($ sa ($ s a))")] ((subst_comp_tel RS sym) RSN 
  21.165      (2,trans)) 1);
  21.166 -by( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1);
  21.167 +by ( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1);
  21.168  by (rtac eq_free_eq_subst_tel 1);
  21.169 -by( safe_tac HOL_cs );
  21.170 +by ( safe_tac HOL_cs );
  21.171  by (subgoal_tac "ma ~= na" 1);
  21.172  by ((forward_tac [new_tv_W] 2) THEN (atac 2));
  21.173  by (etac conjE 2);
  21.174 @@ -367,7 +367,7 @@
  21.175  goal W.thy
  21.176   "!!e. [] |- e :: t' ==>  (? s t. (? m. W e [] n = Ok(s,t,m)) &  \
  21.177  \                                 (? r. t' = $r t))";
  21.178 -by(cut_inst_tac [("a","[]"),("s'","id_subst"),("e","e"),("t'","t'")]
  21.179 +by (cut_inst_tac [("a","[]"),("s'","id_subst"),("e","e"),("t'","t'")]
  21.180                  W_complete_lemma 1);
  21.181 -by(ALLGOALS Asm_full_simp_tac);
  21.182 +by (ALLGOALS Asm_full_simp_tac);
  21.183  qed "W_complete";
    22.1 --- a/src/HOL/Nat.ML	Thu Sep 26 11:11:22 1996 +0200
    22.2 +++ b/src/HOL/Nat.ML	Thu Sep 26 12:47:47 1996 +0200
    22.3 @@ -16,12 +16,12 @@
    22.4  
    22.5  (* Zero is a natural number -- this also justifies the type definition*)
    22.6  goal Nat.thy "Zero_Rep: Nat";
    22.7 -by (rtac (Nat_unfold RS ssubst) 1);
    22.8 +by (stac Nat_unfold 1);
    22.9  by (rtac (singletonI RS UnI1) 1);
   22.10  qed "Zero_RepI";
   22.11  
   22.12  val prems = goal Nat.thy "i: Nat ==> Suc_Rep(i) : Nat";
   22.13 -by (rtac (Nat_unfold RS ssubst) 1);
   22.14 +by (stac Nat_unfold 1);
   22.15  by (rtac (imageI RS UnI2) 1);
   22.16  by (resolve_tac prems 1);
   22.17  qed "Suc_RepI";
   22.18 @@ -293,12 +293,12 @@
   22.19  Addsimps [gr_implies_not0];
   22.20  
   22.21  qed_goal "zero_less_eq" Nat.thy "0 < n = (n ~= 0)" (fn _ => [
   22.22 -	rtac iffI 1,
   22.23 -	etac gr_implies_not0 1,
   22.24 -	rtac natE 1,
   22.25 -	contr_tac 1,
   22.26 -	etac ssubst 1,
   22.27 -	rtac zero_less_Suc 1]);
   22.28 +        rtac iffI 1,
   22.29 +        etac gr_implies_not0 1,
   22.30 +        rtac natE 1,
   22.31 +        contr_tac 1,
   22.32 +        etac ssubst 1,
   22.33 +        rtac zero_less_Suc 1]);
   22.34  
   22.35  (** Inductive (?) properties **)
   22.36  
   22.37 @@ -408,8 +408,8 @@
   22.38  
   22.39  (*
   22.40  goal Nat.thy "(Suc m < n | Suc m = n) = (m < n)";
   22.41 -by(stac (less_Suc_eq RS sym) 1);
   22.42 -by(rtac Suc_less_eq 1);
   22.43 +by (stac (less_Suc_eq RS sym) 1);
   22.44 +by (rtac Suc_less_eq 1);
   22.45  qed "Suc_le_eq";
   22.46  
   22.47  this could make the simpset (with less_Suc_eq added again) more confluent,
   22.48 @@ -562,23 +562,23 @@
   22.49  qed_goalw "Least_Suc" Nat.thy [Least_def]
   22.50   "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
   22.51   (fn _ => [
   22.52 -	rtac select_equality 1,
   22.53 -	fold_goals_tac [Least_def],
   22.54 -	safe_tac (!claset addSEs [LeastI]),
   22.55 -	res_inst_tac [("n","j")] natE 1,
   22.56 -	Fast_tac 1,
   22.57 -	fast_tac (!claset addDs [Suc_less_SucD, not_less_Least]) 1,
   22.58 -	res_inst_tac [("n","k")] natE 1,
   22.59 -	Fast_tac 1,
   22.60 -	hyp_subst_tac 1,
   22.61 -	rewtac Least_def,
   22.62 -	rtac (select_equality RS arg_cong RS sym) 1,
   22.63 -	safe_tac (!claset),
   22.64 -	dtac Suc_mono 1,
   22.65 -	Fast_tac 1,
   22.66 -	cut_facts_tac [less_linear] 1,
   22.67 -	safe_tac (!claset),
   22.68 -	atac 2,
   22.69 -	Fast_tac 2,
   22.70 -	dtac Suc_mono 1,
   22.71 -	Fast_tac 1]);
   22.72 +        rtac select_equality 1,
   22.73 +        fold_goals_tac [Least_def],
   22.74 +        safe_tac (!claset addSEs [LeastI]),
   22.75 +        res_inst_tac [("n","j")] natE 1,
   22.76 +        Fast_tac 1,
   22.77 +        fast_tac (!claset addDs [Suc_less_SucD, not_less_Least]) 1,
   22.78 +        res_inst_tac [("n","k")] natE 1,
   22.79 +        Fast_tac 1,
   22.80 +        hyp_subst_tac 1,
   22.81 +        rewtac Least_def,
   22.82 +        rtac (select_equality RS arg_cong RS sym) 1,
   22.83 +        safe_tac (!claset),
   22.84 +        dtac Suc_mono 1,
   22.85 +        Fast_tac 1,
   22.86 +        cut_facts_tac [less_linear] 1,
   22.87 +        safe_tac (!claset),
   22.88 +        atac 2,
   22.89 +        Fast_tac 2,
   22.90 +        dtac Suc_mono 1,
   22.91 +        Fast_tac 1]);
    23.1 --- a/src/HOL/Option.ML	Thu Sep 26 11:11:22 1996 +0200
    23.2 +++ b/src/HOL/Option.ML	Thu Sep 26 12:47:47 1996 +0200
    23.3 @@ -27,5 +27,5 @@
    23.4  by (option.induct_tac "opt" 1);
    23.5  by (Simp_tac 1);
    23.6  by (Asm_full_simp_tac 1);
    23.7 -by(Fast_tac 1);
    23.8 +by (Fast_tac 1);
    23.9  qed"expand_option_case";
    24.1 --- a/src/HOL/Prod.ML	Thu Sep 26 11:11:22 1996 +0200
    24.2 +++ b/src/HOL/Prod.ML	Thu Sep 26 12:47:47 1996 +0200
    24.3 @@ -331,28 +331,28 @@
    24.4  fun ap_split (Type("*", [T1,T2])) T3 u = 
    24.5        split_const(T1,T2,T3) $ 
    24.6        Abs("v", T1, 
    24.7 -	  ap_split T2 T3
    24.8 -	     ((ap_split T1 (factors T2 ---> T3) (incr_boundvars 1 u)) $ 
    24.9 -	      Bound 0))
   24.10 +          ap_split T2 T3
   24.11 +             ((ap_split T1 (factors T2 ---> T3) (incr_boundvars 1 u)) $ 
   24.12 +              Bound 0))
   24.13    | ap_split T T3 u = u;
   24.14  
   24.15  (*Makes a nested tuple from a list, following the product type structure*)
   24.16  fun mk_tuple (Type("*", [T1,T2])) tms = 
   24.17          mk_Pair (mk_tuple T1 tms, 
   24.18 -		 mk_tuple T2 (drop (length (factors T1), tms)))
   24.19 +                 mk_tuple T2 (drop (length (factors T1), tms)))
   24.20    | mk_tuple T (t::_) = t;
   24.21  
   24.22  (*Attempts to remove occurrences of split, and pair-valued parameters*)
   24.23  val remove_split = rewrite_rule [split RS eq_reflection]  o  
   24.24 -	           rule_by_tactic (ALLGOALS split_all_tac);
   24.25 +                   rule_by_tactic (ALLGOALS split_all_tac);
   24.26  
   24.27  (*Uncurries any Var of function type in the rule*)
   24.28  fun split_rule_var (t as Var(v, Type("fun",[T1,T2])), rl) =
   24.29        let val T' = factors T1 ---> T2
   24.30 -	  val newt = ap_split T1 T2 (Var(v,T'))
   24.31 -	  val cterm = Thm.cterm_of (#sign(rep_thm rl))
   24.32 +          val newt = ap_split T1 T2 (Var(v,T'))
   24.33 +          val cterm = Thm.cterm_of (#sign(rep_thm rl))
   24.34        in
   24.35 -	  remove_split (instantiate ([], [(cterm t, cterm newt)]) rl)
   24.36 +          remove_split (instantiate ([], [(cterm t, cterm newt)]) rl)
   24.37        end
   24.38    | split_rule_var (t,rl) = rl;
   24.39  
    25.1 --- a/src/HOL/RelPow.ML	Thu Sep 26 11:11:22 1996 +0200
    25.2 +++ b/src/HOL/RelPow.ML	Thu Sep 26 12:47:47 1996 +0200
    25.3 @@ -10,7 +10,7 @@
    25.4  Addsimps [rel_pow_0];
    25.5  
    25.6  goal RelPow.thy "R^1 = R";
    25.7 -by(simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
    25.8 +by (simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
    25.9  qed "rel_pow_1";
   25.10  Addsimps [rel_pow_1];
   25.11  
    26.1 --- a/src/HOL/Relation.ML	Thu Sep 26 11:11:22 1996 +0200
    26.2 +++ b/src/HOL/Relation.ML	Thu Sep 26 12:47:47 1996 +0200
    26.3 @@ -104,7 +104,7 @@
    26.4  AddSEs [converseE];
    26.5  
    26.6  goalw Relation.thy [converse_def] "converse(converse R) = R";
    26.7 -by(Fast_tac 1);
    26.8 +by (Fast_tac 1);
    26.9  qed "converse_converse";
   26.10  
   26.11  (** Domain **)
    27.1 --- a/src/HOL/Set.ML	Thu Sep 26 11:11:22 1996 +0200
    27.2 +++ b/src/HOL/Set.ML	Thu Sep 26 12:47:47 1996 +0200
    27.3 @@ -11,7 +11,7 @@
    27.4  section "Relating predicates and sets";
    27.5  
    27.6  val [prem] = goal Set.thy "P(a) ==> a : {x.P(x)}";
    27.7 -by (rtac (mem_Collect_eq RS ssubst) 1);
    27.8 +by (stac mem_Collect_eq 1);
    27.9  by (rtac prem 1);
   27.10  qed "CollectI";
   27.11  
   27.12 @@ -350,10 +350,10 @@
   27.13  bind_thm ("singletonE", make_elim singletonD);
   27.14  
   27.15  qed_goal "singleton_iff" thy "(b : {a}) = (b=a)" (fn _ => [
   27.16 -	rtac iffI 1,
   27.17 -	etac singletonD 1,
   27.18 -	hyp_subst_tac 1,
   27.19 -	rtac singletonI 1]);
   27.20 +        rtac iffI 1,
   27.21 +        etac singletonD 1,
   27.22 +        hyp_subst_tac 1,
   27.23 +        rtac singletonI 1]);
   27.24  
   27.25  val [major] = goal Set.thy "{a}={b} ==> a=b";
   27.26  by (rtac (major RS equalityD1 RS subsetD RS singletonD) 1);
   27.27 @@ -502,7 +502,7 @@
   27.28  
   27.29  
   27.30  val mem_simps = [insert_iff, empty_iff, Un_iff, Int_iff, Compl_iff, Diff_iff, 
   27.31 -		 mem_Collect_eq];
   27.32 +                 mem_Collect_eq];
   27.33  
   27.34  (*Not for Addsimps -- it can cause goals to blow up!*)
   27.35  goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";
    28.1 --- a/src/HOL/Sexp.ML	Thu Sep 26 11:11:22 1996 +0200
    28.2 +++ b/src/HOL/Sexp.ML	Thu Sep 26 12:47:47 1996 +0200
    28.3 @@ -11,17 +11,17 @@
    28.4  (** sexp_case **)
    28.5  
    28.6  goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";
    28.7 -by (resolve_tac [select_equality] 1);
    28.8 +by (rtac select_equality 1);
    28.9  by (ALLGOALS (Fast_tac));
   28.10  qed "sexp_case_Leaf";
   28.11  
   28.12  goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Numb k) = d(k)";
   28.13 -by (resolve_tac [select_equality] 1);
   28.14 +by (rtac select_equality 1);
   28.15  by (ALLGOALS (Fast_tac));
   28.16  qed "sexp_case_Numb";
   28.17  
   28.18  goalw Sexp.thy [sexp_case_def] "sexp_case c d e (M$N) = e M N";
   28.19 -by (resolve_tac [select_equality] 1);
   28.20 +by (rtac select_equality 1);
   28.21  by (ALLGOALS (Fast_tac));
   28.22  qed "sexp_case_Scons";
   28.23  
    29.1 --- a/src/HOL/Trancl.ML	Thu Sep 26 11:11:22 1996 +0200
    29.2 +++ b/src/HOL/Trancl.ML	Thu Sep 26 12:47:47 1996 +0200
    29.3 @@ -116,7 +116,7 @@
    29.4  Addsimps [rtrancl_idemp];
    29.5  
    29.6  goal Trancl.thy "!!r s. r <= s^* ==> r^* <= s^*";
    29.7 -bd rtrancl_mono 1;
    29.8 +by (dtac rtrancl_mono 1);
    29.9  by (Asm_full_simp_tac 1);
   29.10  qed "rtrancl_subset_rtrancl";
   29.11  
   29.12 @@ -163,23 +163,23 @@
   29.13      "[| (a,b) : r^*; P(b); \
   29.14  \       !!y z.[| (y,z) : r;  (z,b) : r^*;  P(z) |] ==> P(y) |]  \
   29.15  \     ==> P(a)";
   29.16 -br ((major RS converseI RS rtrancl_converseI) RS rtrancl_induct) 1;
   29.17 -brs prems 1;
   29.18 -by(fast_tac (!claset addIs prems addSEs[converseD]addSDs[rtrancl_converseD])1);
   29.19 +by (rtac ((major RS converseI RS rtrancl_converseI) RS rtrancl_induct) 1);
   29.20 +by (resolve_tac prems 1);
   29.21 +by (fast_tac (!claset addIs prems addSEs[converseD]addSDs[rtrancl_converseD])1);
   29.22  qed "converse_rtrancl_induct";
   29.23  
   29.24  val prems = goal Trancl.thy
   29.25   "[| ((a,b),(c,d)) : r^*; P c d; \
   29.26  \    !!x y z u.[| ((x,y),(z,u)) : r;  ((z,u),(c,d)) : r^*;  P z u |] ==> P x y\
   29.27  \ |] ==> P a b";
   29.28 -by(res_inst_tac[("R","P")]splitD 1);
   29.29 -by(res_inst_tac[("P","split P")]converse_rtrancl_induct 1);
   29.30 -brs prems 1;
   29.31 -by(Simp_tac 1);
   29.32 -brs prems 1;
   29.33 -by(split_all_tac 1);
   29.34 -by(Asm_full_simp_tac 1);
   29.35 -by(REPEAT(ares_tac prems 1));
   29.36 +by (res_inst_tac[("R","P")]splitD 1);
   29.37 +by (res_inst_tac[("P","split P")]converse_rtrancl_induct 1);
   29.38 +by (resolve_tac prems 1);
   29.39 +by (Simp_tac 1);
   29.40 +by (resolve_tac prems 1);
   29.41 +by (split_all_tac 1);
   29.42 +by (Asm_full_simp_tac 1);
   29.43 +by (REPEAT(ares_tac prems 1));
   29.44  qed "converse_rtrancl_induct2";
   29.45  
   29.46  
    30.1 --- a/src/HOL/WF.ML	Thu Sep 26 11:11:22 1996 +0200
    30.2 +++ b/src/HOL/WF.ML	Thu Sep 26 12:47:47 1996 +0200
    30.3 @@ -129,7 +129,7 @@
    30.4    by (res_inst_tac [("f","cut (%y. H (the_recfun r H y) y) r a1")]
    30.5                     is_the_recfun 1);
    30.6    by (rewtac is_recfun_def);
    30.7 -  by (rtac (cuts_eq RS ssubst) 1);
    30.8 +  by (stac cuts_eq 1);
    30.9    by (rtac allI 1);
   30.10    by (rtac impI 1);
   30.11    by (res_inst_tac [("f1","H"),("x","y")](arg_cong RS fun_cong) 1);
   30.12 @@ -159,7 +159,7 @@
   30.13  by (wf_ind_tac "a" prems 1);
   30.14  by (res_inst_tac [("f", "cut (%y. wftrec r H y) r a1")] is_the_recfun 1); 
   30.15  by (rewrite_goals_tac [is_recfun_def, wftrec_def]);
   30.16 -by (rtac (cuts_eq RS ssubst) 1);
   30.17 +by (stac cuts_eq 1);
   30.18  (*Applying the substitution: must keep the quantified assumption!!*)
   30.19  by (EVERY1 [strip_tac, rtac H_cong1, rtac allE, atac,
   30.20              etac (mp RS ssubst), atac]); 
    31.1 --- a/src/HOL/datatype.ML	Thu Sep 26 11:11:22 1996 +0200
    31.2 +++ b/src/HOL/datatype.ML	Thu Sep 26 12:47:47 1996 +0200
    31.3 @@ -225,7 +225,7 @@
    31.4        val xrules =
    31.5          let val (first_part, scnd_part) = calc_xrules 1 1 cons_list
    31.6          in [Syntax.<-> (("logic", "case x of " ^ first_part),
    31.7 -			("logic", tname ^ "_case " ^ scnd_part ^ " x"))]
    31.8 +                        ("logic", tname ^ "_case " ^ scnd_part ^ " x"))]
    31.9          end;
   31.10  
   31.11       (*type declarations for constructors*)
    32.1 --- a/src/HOL/equalities.ML	Thu Sep 26 11:11:22 1996 +0200
    32.2 +++ b/src/HOL/equalities.ML	Thu Sep 26 12:47:47 1996 +0200
    32.3 @@ -93,8 +93,8 @@
    32.4  goalw Set.thy [image_def]
    32.5  "(%x. if P x then f x else g x) `` S                    \
    32.6  \ = (f `` ({x.x:S & P x})) Un (g `` ({x.x:S & ~(P x)}))";
    32.7 -by(split_tac [expand_if] 1);
    32.8 -by(Fast_tac 1);
    32.9 +by (split_tac [expand_if] 1);
   32.10 +by (Fast_tac 1);
   32.11  qed "if_image_distrib";
   32.12  Addsimps[if_image_distrib];
   32.13  
   32.14 @@ -535,22 +535,22 @@
   32.15    fun prover s = prove_goal Set.thy s (fn _ => [Fast_tac 1])
   32.16  in
   32.17  val UN1_simps = map prover 
   32.18 -		["(UN x. insert a (B x)) = insert a (UN x. B x)",
   32.19 -		 "(UN x. A x Int B)  = ((UN x.A x) Int B)",
   32.20 -		 "(UN x. A Int B x)  = (A Int (UN x.B x))",
   32.21 -		 "(UN x. A x Un B)   = ((UN x.A x) Un B)",
   32.22 -		 "(UN x. A Un B x)   = (A Un (UN x.B x))",
   32.23 -		 "(UN x. A x - B)    = ((UN x.A x) - B)",
   32.24 -		 "(UN x. A - B x)    = (A - (INT x.B x))"];
   32.25 +                ["(UN x. insert a (B x)) = insert a (UN x. B x)",
   32.26 +                 "(UN x. A x Int B)  = ((UN x.A x) Int B)",
   32.27 +                 "(UN x. A Int B x)  = (A Int (UN x.B x))",
   32.28 +                 "(UN x. A x Un B)   = ((UN x.A x) Un B)",
   32.29 +                 "(UN x. A Un B x)   = (A Un (UN x.B x))",
   32.30 +                 "(UN x. A x - B)    = ((UN x.A x) - B)",
   32.31 +                 "(UN x. A - B x)    = (A - (INT x.B x))"];
   32.32  
   32.33  val INT1_simps = map prover
   32.34 -		["(INT x. insert a (B x)) = insert a (INT x. B x)",
   32.35 -		 "(INT x. A x Int B) = ((INT x.A x) Int B)",
   32.36 -		 "(INT x. A Int B x) = (A Int (INT x.B x))",
   32.37 -		 "(INT x. A x Un B)  = ((INT x.A x) Un B)",
   32.38 -		 "(INT x. A Un B x)  = (A Un (INT x.B x))",
   32.39 -		 "(INT x. A x - B)   = ((INT x.A x) - B)",
   32.40 -		 "(INT x. A - B x)   = (A - (UN x.B x))"];
   32.41 +                ["(INT x. insert a (B x)) = insert a (INT x. B x)",
   32.42 +                 "(INT x. A x Int B) = ((INT x.A x) Int B)",
   32.43 +                 "(INT x. A Int B x) = (A Int (INT x.B x))",
   32.44 +                 "(INT x. A x Un B)  = ((INT x.A x) Un B)",
   32.45 +                 "(INT x. A Un B x)  = (A Un (INT x.B x))",
   32.46 +                 "(INT x. A x - B)   = ((INT x.A x) - B)",
   32.47 +                 "(INT x. A - B x)   = (A - (UN x.B x))"];
   32.48  
   32.49  (*Analogous laws for bounded Unions and Intersections are conditional
   32.50    on the index set's being non-empty.  Thus they are probably NOT worth 
    33.1 --- a/src/HOL/ex/Comb.ML	Thu Sep 26 11:11:22 1996 +0200
    33.2 +++ b/src/HOL/ex/Comb.ML	Thu Sep 26 12:47:47 1996 +0200
    33.3 @@ -167,13 +167,13 @@
    33.4  goal Comb.thy "contract^* = parcontract^*";
    33.5  by (REPEAT 
    33.6      (resolve_tac [equalityI, 
    33.7 -		  contract_subset_parcontract RS rtrancl_mono, 
    33.8 -		  parcontract_subset_reduce RS rtrancl_subset_rtrancl] 1));
    33.9 +                  contract_subset_parcontract RS rtrancl_mono, 
   33.10 +                  parcontract_subset_reduce RS rtrancl_subset_rtrancl] 1));
   33.11  qed "reduce_eq_parreduce";
   33.12  
   33.13  goal Comb.thy "diamond(contract^*)";
   33.14  by (simp_tac (!simpset addsimps [reduce_eq_parreduce, diamond_rtrancl, 
   33.15 -			         diamond_parcontract]) 1);
   33.16 +                                 diamond_parcontract]) 1);
   33.17  qed "diamond_reduce";
   33.18  
   33.19  
    34.1 --- a/src/HOL/ex/InSort.ML	Thu Sep 26 11:11:22 1996 +0200
    34.2 +++ b/src/HOL/ex/InSort.ML	Thu Sep 26 12:47:47 1996 +0200
    34.3 @@ -8,37 +8,37 @@
    34.4  
    34.5  goalw InSort.thy [Sorting.total_def]
    34.6    "!!f. [| total(f); ~f x y |] ==> f y x";
    34.7 -by(Fast_tac 1);
    34.8 +by (Fast_tac 1);
    34.9  qed "totalD";
   34.10  
   34.11  goalw InSort.thy [Sorting.transf_def]
   34.12    "!!f. [| transf(f); f b a |] ==> !x. f a x --> f b x";
   34.13 -by(Fast_tac 1);
   34.14 +by (Fast_tac 1);
   34.15  qed "transfD";
   34.16  
   34.17  goal InSort.thy "list_all p (ins f x xs) = (list_all p xs & p(x))";
   34.18 -by(list.induct_tac "xs" 1);
   34.19 -by(Asm_simp_tac 1);
   34.20 -by(asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   34.21 -by(Fast_tac 1);
   34.22 +by (list.induct_tac "xs" 1);
   34.23 +by (Asm_simp_tac 1);
   34.24 +by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   34.25 +by (Fast_tac 1);
   34.26  Addsimps [result()];
   34.27  
   34.28  goal InSort.thy "(!x. p(x) --> q(x)) --> list_all p xs --> list_all q xs";
   34.29 -by(list.induct_tac "xs" 1);
   34.30 -by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   34.31 +by (list.induct_tac "xs" 1);
   34.32 +by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   34.33  qed "list_all_imp";
   34.34  
   34.35  val prems = goal InSort.thy
   34.36    "[| total(f); transf(f) |] ==>  sorted f (ins f x xs) = sorted f xs";
   34.37 -by(list.induct_tac "xs" 1);
   34.38 -by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   34.39 -by(cut_facts_tac prems 1);
   34.40 -by(cut_inst_tac [("p","f(a)"),("q","f(x)")] list_all_imp 1);
   34.41 -by(fast_tac (!claset addDs [totalD,transfD]) 1);
   34.42 +by (list.induct_tac "xs" 1);
   34.43 +by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   34.44 +by (cut_facts_tac prems 1);
   34.45 +by (cut_inst_tac [("p","f(a)"),("q","f(x)")] list_all_imp 1);
   34.46 +by (fast_tac (!claset addDs [totalD,transfD]) 1);
   34.47  Addsimps [result()];
   34.48  
   34.49  goal InSort.thy "!!f. [| total(f); transf(f) |] ==>  sorted f (insort f xs)";
   34.50 -by(list.induct_tac "xs" 1);
   34.51 -by(ALLGOALS Asm_simp_tac);
   34.52 +by (list.induct_tac "xs" 1);
   34.53 +by (ALLGOALS Asm_simp_tac);
   34.54  qed "sorted_insort";
   34.55  
    35.1 --- a/src/HOL/ex/LList.ML	Thu Sep 26 11:11:22 1996 +0200
    35.2 +++ b/src/HOL/ex/LList.ML	Thu Sep 26 12:47:47 1996 +0200
    35.3 @@ -393,7 +393,7 @@
    35.4  
    35.5  AddIs ([Rep_llist]@llist.intrs);
    35.6  AddSDs [inj_onto_Abs_llist RS inj_ontoD,
    35.7 -	inj_Rep_llist RS injD, Leaf_inject];
    35.8 +        inj_Rep_llist RS injD, Leaf_inject];
    35.9  
   35.10  goalw LList.thy [LCons_def] "(LCons x xs=LCons y ys) = (x=y & xs=ys)";
   35.11  by (Fast_tac 1);
   35.12 @@ -648,7 +648,7 @@
   35.13  by (rtac (prem2 RS image_mono RS subset_trans) 1);
   35.14  by (rtac (image_compose RS subst) 1);
   35.15  by (rtac (prod_fun_compose RS subst) 1);
   35.16 -by (rtac (image_Un RS ssubst) 1);
   35.17 +by (stac image_Un 1);
   35.18  by (stac prod_fun_range_eq_diag 1);
   35.19  by (rtac (LListD_Fun_subset_Sigma_llist RS prod_fun_lemma) 1);
   35.20  by (rtac (subset_Sigma_llist RS Un_least) 1);
   35.21 @@ -671,7 +671,7 @@
   35.22       "!!l. (l,l) : llistD_Fun(r Un range(%x.(x,x)))";
   35.23  by (rtac (Rep_llist_inverse RS subst) 1);
   35.24  by (rtac prod_fun_imageI 1);
   35.25 -by (rtac (image_Un RS ssubst) 1);
   35.26 +by (stac image_Un 1);
   35.27  by (stac prod_fun_range_eq_diag 1);
   35.28  by (rtac (Rep_llist RS LListD_Fun_diag_I) 1);
   35.29  qed "llistD_Fun_range_I";
   35.30 @@ -744,7 +744,7 @@
   35.31  qed "lmap_iterates";
   35.32  
   35.33  goal LList.thy "iterates f x = LCons x (lmap f (iterates f x))";
   35.34 -by (rtac (lmap_iterates RS ssubst) 1);
   35.35 +by (stac lmap_iterates 1);
   35.36  by (rtac iterates 1);
   35.37  qed "iterates_lmap";
   35.38  
    36.1 --- a/src/HOL/ex/LexProd.ML	Thu Sep 26 11:11:22 1996 +0200
    36.2 +++ b/src/HOL/ex/LexProd.ML	Thu Sep 26 12:47:47 1996 +0200
    36.3 @@ -10,7 +10,7 @@
    36.4  val prems = goal Prod.thy "!a b. P((a,b)) ==> !p.P(p)";
    36.5  by (cut_facts_tac prems 1);
    36.6  by (rtac allI 1);
    36.7 -by (rtac (surjective_pairing RS ssubst) 1);
    36.8 +by (stac surjective_pairing 1);
    36.9  by (Fast_tac 1);
   36.10  qed "split_all_pair";
   36.11  
    37.1 --- a/src/HOL/ex/Mutil.ML	Thu Sep 26 11:11:22 1996 +0200
    37.2 +++ b/src/HOL/ex/Mutil.ML	Thu Sep 26 12:47:47 1996 +0200
    37.3 @@ -17,8 +17,8 @@
    37.4  by (etac tiling.induct 1);
    37.5  by (Simp_tac 1);
    37.6  by (fast_tac (!claset addIs tiling.intrs
    37.7 -	              addss (HOL_ss addsimps [Un_assoc,
    37.8 -					      subset_empty_iff RS sym])) 1);
    37.9 +                      addss (HOL_ss addsimps [Un_assoc,
   37.10 +                                              subset_empty_iff RS sym])) 1);
   37.11  qed_spec_mp "tiling_UnI";
   37.12  
   37.13  
    38.1 --- a/src/HOL/ex/PropLog.ML	Thu Sep 26 11:11:22 1996 +0200
    38.2 +++ b/src/HOL/ex/PropLog.ML	Thu Sep 26 12:47:47 1996 +0200
    38.3 @@ -18,7 +18,7 @@
    38.4  
    38.5  (*Rule is called I for Identity Combinator, not for Introduction*)
    38.6  goal PropLog.thy "H |- p->p";
    38.7 -by(best_tac (!claset addIs [thms.K,thms.S,thms.MP]) 1);
    38.8 +by (best_tac (!claset addIs [thms.K,thms.S,thms.MP]) 1);
    38.9  qed "thms_I";
   38.10  
   38.11  (** Weakening, left and right **)
   38.12 @@ -35,7 +35,7 @@
   38.13  val weaken_left_Un2  =    Un_upper2 RS weaken_left;
   38.14  
   38.15  goal PropLog.thy "!!H. H |- q ==> H |- p->q";
   38.16 -by(fast_tac (!claset addIs [thms.K,thms.MP]) 1);
   38.17 +by (fast_tac (!claset addIs [thms.K,thms.MP]) 1);
   38.18  qed "weaken_right";
   38.19  
   38.20  (*The deduction theorem*)
   38.21 @@ -43,7 +43,7 @@
   38.22  by (etac thms.induct 1);
   38.23  by (ALLGOALS 
   38.24      (fast_tac (!claset addIs [thms_I, thms.H, thms.K, thms.S, thms.DN, 
   38.25 -			     thms.S RS thms.MP RS thms.MP, weaken_right])));
   38.26 +                             thms.S RS thms.MP RS thms.MP, weaken_right])));
   38.27  qed "deduction";
   38.28  
   38.29  
   38.30 @@ -102,7 +102,7 @@
   38.31  (*This formulation is required for strong induction hypotheses*)
   38.32  goal PropLog.thy "hyps p tt |- (if tt[p] then p else p->false)";
   38.33  by (rtac (expand_if RS iffD2) 1);
   38.34 -by(PropLog.pl.induct_tac "p" 1);
   38.35 +by (PropLog.pl.induct_tac "p" 1);
   38.36  by (ALLGOALS (simp_tac (!simpset addsimps [thms_I, thms.H])));
   38.37  by (fast_tac (!claset addIs [weaken_left_Un1, weaken_left_Un2, 
   38.38                             weaken_right, imp_false]
    39.1 --- a/src/HOL/ex/Puzzle.ML	Thu Sep 26 11:11:22 1996 +0200
    39.2 +++ b/src/HOL/ex/Puzzle.ML	Thu Sep 26 12:47:47 1996 +0200
    39.3 @@ -22,7 +22,7 @@
    39.4  by (dtac not_leE 1);
    39.5  by (subgoal_tac "f(na) <= f(f(na))" 1);
    39.6  by (fast_tac (!claset addIs [Puzzle.f_ax]) 2);
    39.7 -br lessD 1;
    39.8 +by (rtac lessD 1);
    39.9  by (best_tac (!claset delrules [le_refl] 
   39.10                        addIs [Puzzle.f_ax, le_less_trans]) 1);
   39.11  val lemma = result() RS spec RS mp;
    40.1 --- a/src/HOL/ex/Qsort.ML	Thu Sep 26 11:11:22 1996 +0200
    40.2 +++ b/src/HOL/ex/Qsort.ML	Thu Sep 26 12:47:47 1996 +0200
    40.3 @@ -9,40 +9,40 @@
    40.4  Addsimps ([Qsort.qsort_Nil,Qsort.qsort_Cons]@conj_comms);
    40.5  
    40.6  goal Qsort.thy "!x. mset (qsort le xs) x = mset xs x";
    40.7 -by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
    40.8 -by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
    40.9 +by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
   40.10 +by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   40.11  result();
   40.12  
   40.13  
   40.14  goal Qsort.thy "(Alls x:[x:xs.P(x)].Q(x)) = (Alls x:xs. P(x)-->Q(x))";
   40.15 -by(list.induct_tac "xs" 1);
   40.16 -by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   40.17 +by (list.induct_tac "xs" 1);
   40.18 +by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   40.19  Addsimps [result()];
   40.20  
   40.21  goal Qsort.thy
   40.22   "((Alls x:xs.P(x)) & (Alls x:xs.Q(x))) = (Alls x:xs. P(x)&Q(x))";
   40.23 -by(list.induct_tac "xs" 1);
   40.24 -by(ALLGOALS Asm_simp_tac);
   40.25 +by (list.induct_tac "xs" 1);
   40.26 +by (ALLGOALS Asm_simp_tac);
   40.27  val alls_lemma=result();
   40.28  Addsimps [alls_lemma];
   40.29  
   40.30  goal HOL.thy "((P --> Q) & (~P --> Q)) = Q";
   40.31 -by(Fast_tac 1);
   40.32 +by (Fast_tac 1);
   40.33  val lemma = result();
   40.34  
   40.35  goal Qsort.thy "(Alls x:qsort le xs.P(x))  =  (Alls x:xs.P(x))";
   40.36 -by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
   40.37 -by(Asm_simp_tac 1);
   40.38 -by(asm_simp_tac (!simpset delsimps [alls_lemma, list_all_Cons])1);
   40.39 -by(asm_simp_tac (!simpset addsimps [lemma]) 1);
   40.40 +by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
   40.41 +by (Asm_simp_tac 1);
   40.42 +by (asm_simp_tac (!simpset delsimps [alls_lemma, list_all_Cons])1);
   40.43 +by (asm_simp_tac (!simpset addsimps [lemma]) 1);
   40.44  Addsimps [result()];
   40.45  
   40.46  goal Qsort.thy
   40.47   "sorted le (xs@ys) = (sorted le xs & sorted le ys & \
   40.48  \                     (Alls x:xs. Alls y:ys. le x y))";
   40.49 -by(list.induct_tac "xs" 1);
   40.50 -by(Asm_simp_tac 1);
   40.51 -by(asm_simp_tac (!simpset delsimps [alls_lemma]) 1);
   40.52 +by (list.induct_tac "xs" 1);
   40.53 +by (Asm_simp_tac 1);
   40.54 +by (asm_simp_tac (!simpset delsimps [alls_lemma]) 1);
   40.55  Addsimps [result()];
   40.56  
   40.57  
   40.58 @@ -50,12 +50,12 @@
   40.59  
   40.60  goal Qsort.thy 
   40.61   "!!le. [| total(le); transf(le) |] ==>  sorted le (qsort le xs)";
   40.62 -by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
   40.63 -by(Asm_simp_tac 1);
   40.64 -by(asm_full_simp_tac (!simpset addsimps []) 1);
   40.65 -by(asm_full_simp_tac (!simpset addsimps [list_all_mem_conv]) 1);
   40.66 -by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]);
   40.67 -by(Fast_tac 1);
   40.68 +by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
   40.69 +by (Asm_simp_tac 1);
   40.70 +by (asm_full_simp_tac (!simpset addsimps []) 1);
   40.71 +by (asm_full_simp_tac (!simpset addsimps [list_all_mem_conv]) 1);
   40.72 +by (rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]);
   40.73 +by (Fast_tac 1);
   40.74  result();
   40.75  
   40.76  (* A verification based on predicate calculus rather than combinators *)
   40.77 @@ -67,31 +67,31 @@
   40.78  
   40.79  
   40.80  goal Qsort.thy "x mem qsort le xs = x mem xs";
   40.81 -by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
   40.82 -by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   40.83 -by(Fast_tac 1);
   40.84 +by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
   40.85 +by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   40.86 +by (Fast_tac 1);
   40.87  Addsimps [result()];
   40.88  
   40.89  goal Qsort.thy
   40.90   "sorted le (xs@ys) = (sorted le xs & sorted le ys & \
   40.91  \                     (!x. x mem xs --> (!y. y mem ys --> le x y)))";
   40.92 -by(list.induct_tac "xs" 1);
   40.93 -by(Asm_simp_tac 1);
   40.94 -by(asm_simp_tac (!simpset setloop (split_tac [expand_if])
   40.95 -			  delsimps [list_all_conj]
   40.96 -			  addsimps [list_all_mem_conv]) 1);
   40.97 -by(Fast_tac 1);
   40.98 +by (list.induct_tac "xs" 1);
   40.99 +by (Asm_simp_tac 1);
  40.100 +by (asm_simp_tac (!simpset setloop (split_tac [expand_if])
  40.101 +                          delsimps [list_all_conj]
  40.102 +                          addsimps [list_all_mem_conv]) 1);
  40.103 +by (Fast_tac 1);
  40.104  Addsimps [result()];
  40.105  
  40.106  goal Qsort.thy
  40.107    "!!xs. [| total(le); transf(le) |] ==>  sorted le (qsort le xs)";
  40.108 -by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
  40.109 -by(Simp_tac 1);
  40.110 -by(asm_simp_tac (!simpset setloop (split_tac [expand_if])
  40.111 -			  delsimps [list_all_conj]
  40.112 -			  addsimps [list_all_mem_conv]) 1);
  40.113 -by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]);
  40.114 -by(Fast_tac 1);
  40.115 +by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
  40.116 +by (Simp_tac 1);
  40.117 +by (asm_simp_tac (!simpset setloop (split_tac [expand_if])
  40.118 +                          delsimps [list_all_conj]
  40.119 +                          addsimps [list_all_mem_conv]) 1);
  40.120 +by (rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]);
  40.121 +by (Fast_tac 1);
  40.122  result();
  40.123  
  40.124  
    41.1 --- a/src/HOL/ex/SList.ML	Thu Sep 26 11:11:22 1996 +0200
    41.2 +++ b/src/HOL/ex/SList.ML	Thu Sep 26 12:47:47 1996 +0200
    41.3 @@ -125,10 +125,10 @@
    41.4  
    41.5  
    41.6  goal SList.thy "(xs ~= []) = (? y ys. xs = y#ys)";
    41.7 -by(list_ind_tac "xs" 1);
    41.8 -by(Simp_tac 1);
    41.9 -by(Asm_simp_tac 1);
   41.10 -by(REPEAT(resolve_tac [exI,refl,conjI] 1));
   41.11 +by (list_ind_tac "xs" 1);
   41.12 +by (Simp_tac 1);
   41.13 +by (Asm_simp_tac 1);
   41.14 +by (REPEAT(resolve_tac [exI,refl,conjI] 1));
   41.15  qed "neq_Nil_conv2";
   41.16  
   41.17  (** Conversion rules for List_case: case analysis operator **)
   41.18 @@ -243,7 +243,7 @@
   41.19  
   41.20  goalw SList.thy [Rep_map_def] "!!f. (!!x. f(x): A) ==> Rep_map f xs: list(A)";
   41.21  by (rtac list_induct2 1);
   41.22 -by(ALLGOALS Asm_simp_tac);
   41.23 +by (ALLGOALS Asm_simp_tac);
   41.24  qed "Rep_map_type";
   41.25  
   41.26  goalw SList.thy [Abs_map_def] "Abs_map g NIL = Nil";
   41.27 @@ -275,16 +275,16 @@
   41.28  
   41.29  (*** Unfolding the basic combinators ***)
   41.30  
   41.31 -val [null_Nil, null_Cons] 		= list_recs null_def;
   41.32 -val [_, hd_Cons]			= list_recs hd_def;
   41.33 -val [_, tl_Cons]			= list_recs tl_def;
   41.34 -val [ttl_Nil, ttl_Cons]			= list_recs ttl_def;
   41.35 -val [append_Nil3, append_Cons] 		= list_recs append_def;
   41.36 -val [mem_Nil, mem_Cons] 		= list_recs mem_def;
   41.37 -val [set_of_list_Nil, set_of_list_Cons]	= list_recs set_of_list_def;
   41.38 -val [map_Nil, map_Cons]			= list_recs map_def;
   41.39 -val [list_case_Nil, list_case_Cons] 	= list_recs list_case_def;
   41.40 -val [filter_Nil, filter_Cons]		= list_recs filter_def;
   41.41 +val [null_Nil, null_Cons]               = list_recs null_def;
   41.42 +val [_, hd_Cons]                        = list_recs hd_def;
   41.43 +val [_, tl_Cons]                        = list_recs tl_def;
   41.44 +val [ttl_Nil, ttl_Cons]                 = list_recs ttl_def;
   41.45 +val [append_Nil3, append_Cons]          = list_recs append_def;
   41.46 +val [mem_Nil, mem_Cons]                 = list_recs mem_def;
   41.47 +val [set_of_list_Nil, set_of_list_Cons] = list_recs set_of_list_def;
   41.48 +val [map_Nil, map_Cons]                 = list_recs map_def;
   41.49 +val [list_case_Nil, list_case_Cons]     = list_recs list_case_def;
   41.50 +val [filter_Nil, filter_Cons]           = list_recs filter_def;
   41.51  
   41.52  Addsimps
   41.53    [null_Nil, ttl_Nil,
   41.54 @@ -299,25 +299,25 @@
   41.55  (** @ - append **)
   41.56  
   41.57  goal SList.thy "(xs@ys)@zs = xs@(ys@zs)";
   41.58 -by(list_ind_tac "xs" 1);
   41.59 -by(ALLGOALS Asm_simp_tac);
   41.60 +by (list_ind_tac "xs" 1);
   41.61 +by (ALLGOALS Asm_simp_tac);
   41.62  qed "append_assoc2";
   41.63  
   41.64  goal SList.thy "xs @ [] = xs";
   41.65 -by(list_ind_tac "xs" 1);
   41.66 -by(ALLGOALS Asm_simp_tac);
   41.67 +by (list_ind_tac "xs" 1);
   41.68 +by (ALLGOALS Asm_simp_tac);
   41.69  qed "append_Nil4";
   41.70  
   41.71  (** mem **)
   41.72  
   41.73  goal SList.thy "x mem (xs@ys) = (x mem xs | x mem ys)";
   41.74 -by(list_ind_tac "xs" 1);
   41.75 -by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   41.76 +by (list_ind_tac "xs" 1);
   41.77 +by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   41.78  qed "mem_append2";
   41.79  
   41.80  goal SList.thy "x mem [x:xs.P(x)] = (x mem xs & P(x))";
   41.81 -by(list_ind_tac "xs" 1);
   41.82 -by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   41.83 +by (list_ind_tac "xs" 1);
   41.84 +by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   41.85  qed "mem_filter2";
   41.86  
   41.87  
   41.88 @@ -339,9 +339,9 @@
   41.89  goal SList.thy
   41.90   "P(list_case a f xs) = ((xs=[] --> P(a)) & \
   41.91  \                        (!y ys. xs=y#ys --> P(f y ys)))";
   41.92 -by(list_ind_tac "xs" 1);
   41.93 -by(ALLGOALS Asm_simp_tac);
   41.94 -by(Fast_tac 1);
   41.95 +by (list_ind_tac "xs" 1);
   41.96 +by (ALLGOALS Asm_simp_tac);
   41.97 +by (Fast_tac 1);
   41.98  qed "expand_list_case2";
   41.99  
  41.100  
  41.101 @@ -365,7 +365,7 @@
  41.102  goal SList.thy "!!f. (!!x. f(x): sexp) ==> \
  41.103  \       Abs_map g (Rep_map f xs) = map (%t. g(f(t))) xs";
  41.104  by (list_ind_tac "xs" 1);
  41.105 -by(ALLGOALS(asm_simp_tac(!simpset addsimps
  41.106 +by (ALLGOALS(asm_simp_tac(!simpset addsimps
  41.107         [Rep_map_type,list_sexp RS subsetD])));
  41.108  qed "Abs_Rep_map";
  41.109  
    42.1 --- a/src/HOL/ex/Sorting.ML	Thu Sep 26 11:11:22 1996 +0200
    42.2 +++ b/src/HOL/ex/Sorting.ML	Thu Sep 26 12:47:47 1996 +0200
    42.3 @@ -11,14 +11,14 @@
    42.4            Sorting.sorted1_Nil,Sorting.sorted1_One,Sorting.sorted1_Cons];
    42.5  
    42.6  goal Sorting.thy "!x.mset (xs@ys) x = mset xs x + mset ys x";
    42.7 -by(list.induct_tac "xs" 1);
    42.8 -by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
    42.9 +by (list.induct_tac "xs" 1);
   42.10 +by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   42.11  qed "mset_app_distr";
   42.12  
   42.13  goal Sorting.thy "!x. mset [x:xs. ~p(x)] x + mset [x:xs.p(x)] x = \
   42.14  \                     mset xs x";
   42.15 -by(list.induct_tac "xs" 1);
   42.16 -by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   42.17 +by (list.induct_tac "xs" 1);
   42.18 +by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   42.19  qed "mset_compl_add";
   42.20  
   42.21  Addsimps [mset_app_distr, mset_compl_add];
    43.1 --- a/src/HOL/ex/String.ML	Thu Sep 26 11:11:22 1996 +0200
    43.2 +++ b/src/HOL/ex/String.ML	Thu Sep 26 12:47:47 1996 +0200
    43.3 @@ -1,20 +1,20 @@
    43.4  goal String.thy "hd(''ABCD'') = CHR ''A''";
    43.5 -by(Simp_tac 1);
    43.6 +by (Simp_tac 1);
    43.7  result();
    43.8  
    43.9  goal String.thy "hd(''ABCD'') ~= CHR ''B''";
   43.10 -by(Simp_tac 1);
   43.11 +by (Simp_tac 1);
   43.12  result();
   43.13  
   43.14  goal String.thy "''ABCD'' ~= ''ABCX''";
   43.15 -by(Simp_tac 1);
   43.16 +by (Simp_tac 1);
   43.17  result();
   43.18  
   43.19  goal String.thy "''ABCD'' = ''ABCD''";
   43.20 -by(Simp_tac 1);
   43.21 +by (Simp_tac 1);
   43.22  result();
   43.23  
   43.24  goal String.thy
   43.25    "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''";
   43.26 -by(Simp_tac 1);
   43.27 +by (Simp_tac 1);
   43.28  result();
    44.1 --- a/src/HOL/ex/meson.ML	Thu Sep 26 11:11:22 1996 +0200
    44.2 +++ b/src/HOL/ex/meson.ML	Thu Sep 26 12:47:47 1996 +0200
    44.3 @@ -189,10 +189,10 @@
    44.4  fun skolemize th = 
    44.5    if not (has_consts ["Ex"] (prop_of th)) then th
    44.6    else skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
    44.7 -			      disj_exD, disj_exD1, disj_exD2]))
    44.8 +                              disj_exD, disj_exD1, disj_exD2]))
    44.9      handle THM _ => 
   44.10          skolemize (forward_res skolemize
   44.11 -		   (tryres (th, [conj_forward, disj_forward, all_forward])))
   44.12 +                   (tryres (th, [conj_forward, disj_forward, all_forward])))
   44.13      handle THM _ => forward_res skolemize (th RS ex_forward);
   44.14  
   44.15  
   44.16 @@ -211,7 +211,7 @@
   44.17    | taut_lits ((flg,t)::ts) = (not flg,t) mem ts orelse taut_lits ts;
   44.18  
   44.19  val term_False = term_of (read_cterm (sign_of HOL.thy) 
   44.20 -			  ("False", Type("bool",[])));
   44.21 +                          ("False", Type("bool",[])));
   44.22  
   44.23  (*Include False as a literal: an occurrence of ~False is a tautology*)
   44.24  fun is_taut th = taut_lits ((true,term_False) :: literals (prop_of th));
   44.25 @@ -272,8 +272,8 @@
   44.26  fun forward_res2 nf hyps st =
   44.27    case Sequence.pull
   44.28          (REPEAT 
   44.29 -	 (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1) 
   44.30 -	 st)
   44.31 +         (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1) 
   44.32 +         st)
   44.33    of Some(th,_) => th
   44.34     | None => raise THM("forward_res2", 0, [st]);
   44.35  
   44.36 @@ -426,7 +426,7 @@
   44.37    MESON (fn cls => 
   44.38           THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
   44.39                           (has_fewer_prems 1, sizef)
   44.40 -			 (prolog_step_tac (make_horns cls) 1));
   44.41 +                         (prolog_step_tac (make_horns cls) 1));
   44.42  
   44.43  (*First, breaks the goal into independent units*)
   44.44  val safe_best_meson_tac =
   44.45 @@ -451,7 +451,7 @@
   44.46          val nrtac = net_resolve_tac horns
   44.47      in  fn i => eq_assume_tac i ORELSE
   44.48                  match_tac horn0s i ORELSE  (*no backtracking if unit MATCHES*)
   44.49 -	        ((assume_tac i APPEND nrtac i) THEN check_tac)
   44.50 +                ((assume_tac i APPEND nrtac i) THEN check_tac)
   44.51      end;
   44.52  
   44.53  fun iter_deepen_prolog_tac horns = 
   44.54 @@ -460,8 +460,8 @@
   44.55  val iter_deepen_meson_tac = 
   44.56    MESON (fn cls => 
   44.57           (THEN_ITER_DEEPEN (resolve_tac (gocls cls) 1)
   44.58 -	                   (has_fewer_prems 1)
   44.59 -	                   (prolog_step_tac' (make_horns cls))));
   44.60 +                           (has_fewer_prems 1)
   44.61 +                           (prolog_step_tac' (make_horns cls))));
   44.62  
   44.63  val safe_meson_tac =
   44.64       SELECT_GOAL (TRY (safe_tac (!claset)) THEN 
    45.1 --- a/src/HOL/ex/mesontest.ML	Thu Sep 26 11:11:22 1996 +0200
    45.2 +++ b/src/HOL/ex/mesontest.ML	Thu Sep 26 12:47:47 1996 +0200
    45.3 @@ -326,7 +326,7 @@
    45.4  by (safe_meson_tac 1); 
    45.5  result();
    45.6  
    45.7 -writeln"Problem 27";	(*13 Horn clauses*)
    45.8 +writeln"Problem 27";    (*13 Horn clauses*)
    45.9  goal HOL.thy "(? x. P x & ~Q x) &   \
   45.10  \             (! x. P x --> R x) &   \
   45.11  \             (! x. M x & L x --> P x) &   \
   45.12 @@ -335,7 +335,7 @@
   45.13  by (safe_meson_tac 1); 
   45.14  result();
   45.15  
   45.16 -writeln"Problem 28.  AMENDED";	(*14 Horn clauses*)
   45.17 +writeln"Problem 28.  AMENDED";  (*14 Horn clauses*)
   45.18  goal HOL.thy "(! x. P x --> (! x. Q x)) &   \
   45.19  \       ((! x. Q x | R x) --> (? x. Q x & S x)) &  \
   45.20  \       ((? x.S x) --> (! x. L x --> M x))  \
   45.21 @@ -344,7 +344,7 @@
   45.22  result();
   45.23  
   45.24  writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";
   45.25 -	(*62 Horn clauses*)
   45.26 +        (*62 Horn clauses*)
   45.27  goal HOL.thy "(? x. F x) & (? y. G y)  \
   45.28  \   --> ( ((! x. F x --> H x) & (! y. G y --> J y))  =   \
   45.29  \         (! x y. F x & G y --> H x & J y))";
   45.30 @@ -447,7 +447,7 @@
   45.31  writeln"Problem 43  NOW PROVED AUTOMATICALLY!!";
   45.32  goal HOL.thy "(! x. ! y. q x y = (! z. p z x = (p z y::bool)))  \
   45.33  \         --> (! x. (! y. q x y = (q y x::bool)))";
   45.34 -by (safe_best_meson_tac 1);	
   45.35 +by (safe_best_meson_tac 1);     
   45.36  (*1.6 secs; iter. deepening is slightly slower*)
   45.37  result();
   45.38  
   45.39 @@ -466,7 +466,7 @@
   45.40  \     (? x. f x & (! y. h x y --> l y)                        \
   45.41  \                  & (! y. g y & h x y --> j x y))             \
   45.42  \     --> (? x. f x & ~ (? y. g y & h x y))";
   45.43 -by (safe_best_meson_tac 1);	
   45.44 +by (safe_best_meson_tac 1);     
   45.45  (*1.6 secs; iter. deepening is slightly slower*)
   45.46  result();
   45.47  
   45.48 @@ -477,12 +477,12 @@
   45.49  \     (? x. f x & ~g x & (! y. f y & ~g y --> j x y))) &    \
   45.50  \    (! x y. f x & f y & h x y --> ~j y x)                    \
   45.51  \     --> (! x. f x --> g x)";
   45.52 -by (safe_best_meson_tac 1);	
   45.53 +by (safe_best_meson_tac 1);     
   45.54  (*1.7 secs; iter. deepening is slightly slower*)
   45.55  result();
   45.56  
   45.57  writeln"Problem 47.  Schubert's Steamroller";
   45.58 -	(*26 clauses; 63 Horn clauses*)
   45.59 +        (*26 clauses; 63 Horn clauses*)
   45.60  goal HOL.thy
   45.61      "(! x. P1 x --> P0 x) & (? x.P1 x) &     \
   45.62  \    (! x. P2 x --> P0 x) & (? x.P2 x) &     \
   45.63 @@ -501,7 +501,7 @@
   45.64  \    (! x y. P3 x & P5 y --> ~R x y) &       \
   45.65  \    (! x. (P4 x|P5 x) --> (? y.Q0 y & R x y))      \
   45.66  \    --> (? x y. P0 x & P0 y & (? z. Q1 z & R y z & R x y))";
   45.67 -by (safe_meson_tac 1);	 (*119 secs*)
   45.68 +by (safe_meson_tac 1);   (*119 secs*)
   45.69  result();
   45.70  
   45.71  (*The Los problem?  Circulated by John Harrison*)
   45.72 @@ -510,7 +510,7 @@
   45.73  \      (! x y. P x y --> P y x) &       \
   45.74  \      (! (x::'a) y. P x y | Q x y)     \
   45.75  \      --> (! x y. P x y) | (! x y. Q x y)";
   45.76 -by (safe_best_meson_tac 1);	(*3 secs; iter. deepening is VERY slow*)
   45.77 +by (safe_best_meson_tac 1);     (*3 secs; iter. deepening is VERY slow*)
   45.78  result();
   45.79  
   45.80  (*A similar example, suggested by Johannes Schumann and credited to Pelletier*)
    46.1 --- a/src/HOL/ex/set.ML	Thu Sep 26 11:11:22 1996 +0200
    46.2 +++ b/src/HOL/ex/set.ML	Thu Sep 26 12:47:47 1996 +0200
    46.3 @@ -12,7 +12,7 @@
    46.4  (*** A unique fixpoint theorem --- fast/best/meson all fail ***)
    46.5  
    46.6  val [prem] = goal HOL.thy "?!x.f(g(x))=x ==> ?!y.g(f(y))=y";
    46.7 -by(EVERY1[rtac (prem RS ex1E), rtac ex1I, etac arg_cong,
    46.8 +by (EVERY1[rtac (prem RS ex1E), rtac ex1I, etac arg_cong,
    46.9            rtac subst, atac, etac allE, rtac arg_cong, etac mp, etac arg_cong]);
   46.10  result();
   46.11  
   46.12 @@ -92,7 +92,7 @@
   46.13  \       bij = (%z. if z:X then f(z) else g(z)) |] ==> \
   46.14  \       inj(bij) & surj(bij)";
   46.15  val f_eq_gE = make_elim (compl RS disj_lemma);
   46.16 -by (rtac (bij RS ssubst) 1);
   46.17 +by (stac bij 1);
   46.18  by (rtac conjI 1);
   46.19  by (rtac (compl RS surj_if_then_else) 2);
   46.20  by (rewtac inj_def);
    47.1 --- a/src/HOL/ex/unsolved.ML	Thu Sep 26 11:11:22 1996 +0200
    47.2 +++ b/src/HOL/ex/unsolved.ML	Thu Sep 26 12:47:47 1996 +0200
    47.3 @@ -7,7 +7,7 @@
    47.4  *)
    47.5  
    47.6  (*from Vladimir Lifschitz, What Is the Inverse Method?, JAR 5  1989.  1--23*)
    47.7 -	(*27 clauses; 81 Horn clauses*)
    47.8 +        (*27 clauses; 81 Horn clauses*)
    47.9  goal HOL.thy "? x x'. ! y. ? z z'. (~P y y | P x x | ~S z x) & \
   47.10  \                                  (S x y | ~S y z | Q z' z')  & \
   47.11  \                                  (Q x' y | ~Q y z' | S x' x')";
   47.12 @@ -32,7 +32,7 @@
   47.13  \  killed agatha agatha";
   47.14  
   47.15  (*Halting problem: Formulation of Li Dafa (AAR Newsletter 27, Oct 1994.)
   47.16 -	author U. Egly;  46 clauses; 264 Horn clauses*)
   47.17 +        author U. Egly;  46 clauses; 264 Horn clauses*)
   47.18  goal HOL.thy
   47.19   "((EX X. (a X) & (ALL Y. (c Y) --> (ALL Z. (d X Y Z)))) -->  \
   47.20  \  (EX W. (c W) & (ALL Y. (c Y) --> (ALL Z. (d W Y Z)))))     \
    48.1 --- a/src/HOL/indrule.ML	Thu Sep 26 11:11:22 1996 +0200
    48.2 +++ b/src/HOL/indrule.ML	Thu Sep 26 12:47:47 1996 +0200
    48.3 @@ -120,7 +120,7 @@
    48.4  fun mk_predpair rec_tm = 
    48.5    let val rec_name = (#1 o dest_Const o head_of) rec_tm
    48.6        val pfree = Free(pred_name ^ "_" ^ rec_name, 
    48.7 -		       elem_factors ---> Ind_Syntax.boolT)
    48.8 +                       elem_factors ---> Ind_Syntax.boolT)
    48.9        val qconcl = 
   48.10          foldr Ind_Syntax.mk_all 
   48.11            (elem_frees, 
   48.12 @@ -148,8 +148,8 @@
   48.13      Ind_Syntax.mk_Trueprop (fold_bal (app Ind_Syntax.conj) qconcls);
   48.14  
   48.15  val lemma_tac = FIRST' [eresolve_tac [asm_rl, conjE, PartE, mp],
   48.16 -			resolve_tac [allI, impI, conjI, Part_eqI, refl],
   48.17 -			dresolve_tac [spec, mp, splitD]];
   48.18 +                        resolve_tac [allI, impI, conjI, Part_eqI, refl],
   48.19 +                        dresolve_tac [spec, mp, splitD]];
   48.20  
   48.21  val lemma = (*makes the link between the two induction rules*)
   48.22      prove_goalw_cterm part_rec_defs 
   48.23 @@ -158,7 +158,7 @@
   48.24            (fn prems =>
   48.25             [cut_facts_tac prems 1,
   48.26              REPEAT (rewrite_goals_tac [split RS eq_reflection] THEN
   48.27 -		    lemma_tac 1)])
   48.28 +                    lemma_tac 1)])
   48.29      handle e => print_sign_exn sign e;
   48.30  
   48.31  (*Mutual induction follows by freeness of Inl/Inr.*)
   48.32 @@ -223,8 +223,8 @@
   48.33    struct
   48.34    val induct = standard 
   48.35                    (Prod_Syntax.split_rule_var
   48.36 -		    (Var((pred_name,2), elem_type --> Ind_Syntax.boolT),
   48.37 -		     induct0));
   48.38 +                    (Var((pred_name,2), elem_type --> Ind_Syntax.boolT),
   48.39 +                     induct0));
   48.40  
   48.41    (*Just "True" unless there's true mutual recursion.  This saves storage.*)
   48.42    val mutual_induct = 
    49.1 --- a/src/HOL/intr_elim.ML	Thu Sep 26 11:11:22 1996 +0200
    49.2 +++ b/src/HOL/intr_elim.ML	Thu Sep 26 12:47:47 1996 +0200
    49.3 @@ -82,7 +82,7 @@
    49.4  fun intro_tacsf disjIn prems = 
    49.5    [(*insert prems and underlying sets*)
    49.6     cut_facts_tac prems 1,
    49.7 -   rtac (unfold RS ssubst) 1,
    49.8 +   stac unfold 1,
    49.9     REPEAT (resolve_tac [Part_eqI,CollectI] 1),
   49.10     (*Now 1-2 subgoals: the disjunction, perhaps equality.*)
   49.11     rtac disjIn 1,
    50.1 --- a/src/HOL/simpdata.ML	Thu Sep 26 11:11:22 1996 +0200
    50.2 +++ b/src/HOL/simpdata.ML	Thu Sep 26 12:47:47 1996 +0200
    50.3 @@ -33,8 +33,8 @@
    50.4  (*** Addition of rules to simpsets and clasets simultaneously ***)
    50.5  
    50.6  (*Takes UNCONDITIONAL theorems of the form A<->B to 
    50.7 -	the Safe Intr     rule B==>A and 
    50.8 -	the Safe Destruct rule A==>B.
    50.9 +        the Safe Intr     rule B==>A and 
   50.10 +        the Safe Destruct rule A==>B.
   50.11    Also ~A goes to the Safe Elim rule A ==> ?R
   50.12    Failing other cases, A is added as a Safe Intr rule*)
   50.13  local
   50.14 @@ -42,31 +42,31 @@
   50.15  
   50.16    fun addIff th = 
   50.17        (case HOLogic.dest_Trueprop (#prop(rep_thm th)) of
   50.18 -		(Const("not",_) $ A) =>
   50.19 -		    AddSEs [zero_var_indexes (th RS notE)]
   50.20 -	      | (con $ _ $ _) =>
   50.21 -		    if con=iff_const
   50.22 -		    then (AddSIs [zero_var_indexes (th RS iffD2)];  
   50.23 -			  AddSDs [zero_var_indexes (th RS iffD1)])
   50.24 -		    else  AddSIs [th]
   50.25 -	      | _ => AddSIs [th];
   50.26 +                (Const("not",_) $ A) =>
   50.27 +                    AddSEs [zero_var_indexes (th RS notE)]
   50.28 +              | (con $ _ $ _) =>
   50.29 +                    if con=iff_const
   50.30 +                    then (AddSIs [zero_var_indexes (th RS iffD2)];  
   50.31 +                          AddSDs [zero_var_indexes (th RS iffD1)])
   50.32 +                    else  AddSIs [th]
   50.33 +              | _ => AddSIs [th];
   50.34         Addsimps [th])
   50.35        handle _ => error ("AddIffs: theorem must be unconditional\n" ^ 
   50.36 -			 string_of_thm th)
   50.37 +                         string_of_thm th)
   50.38  
   50.39    fun delIff th = 
   50.40        (case HOLogic.dest_Trueprop (#prop(rep_thm th)) of
   50.41 -		(Const("not",_) $ A) =>
   50.42 -		    Delrules [zero_var_indexes (th RS notE)]
   50.43 -	      | (con $ _ $ _) =>
   50.44 -		    if con=iff_const
   50.45 -		    then Delrules [zero_var_indexes (th RS iffD2),
   50.46 -				   zero_var_indexes (th RS iffD1)]
   50.47 -		    else Delrules [th]
   50.48 -	      | _ => Delrules [th];
   50.49 +                (Const("not",_) $ A) =>
   50.50 +                    Delrules [zero_var_indexes (th RS notE)]
   50.51 +              | (con $ _ $ _) =>
   50.52 +                    if con=iff_const
   50.53 +                    then Delrules [zero_var_indexes (th RS iffD2),
   50.54 +                                   zero_var_indexes (th RS iffD1)]
   50.55 +                    else Delrules [th]
   50.56 +              | _ => Delrules [th];
   50.57         Delsimps [th])
   50.58        handle _ => warning("DelIffs: ignoring conditional theorem\n" ^ 
   50.59 -			  string_of_thm th)
   50.60 +                          string_of_thm th)
   50.61  in
   50.62  val AddIffs = seq addIff
   50.63  val DelIffs = seq delIff
   50.64 @@ -85,19 +85,19 @@
   50.65  
   50.66    fun atomize pairs =
   50.67      let fun atoms th =
   50.68 -	  (case concl_of th of
   50.69 -	     Const("Trueprop",_) $ p =>
   50.70 -	       (case head_of p of
   50.71 -		  Const(a,_) =>
   50.72 -		    (case assoc(pairs,a) of
   50.73 -		       Some(rls) => flat (map atoms ([th] RL rls))
   50.74 -		     | None => [th])
   50.75 -		| _ => [th])
   50.76 -	   | _ => [th])
   50.77 +          (case concl_of th of
   50.78 +             Const("Trueprop",_) $ p =>
   50.79 +               (case head_of p of
   50.80 +                  Const(a,_) =>
   50.81 +                    (case assoc(pairs,a) of
   50.82 +                       Some(rls) => flat (map atoms ([th] RL rls))
   50.83 +                     | None => [th])
   50.84 +                | _ => [th])
   50.85 +           | _ => [th])
   50.86      in atoms end;
   50.87  
   50.88    fun mk_meta_eq r = case concl_of r of
   50.89 -	  Const("==",_)$_$_ => r
   50.90 +          Const("==",_)$_$_ => r
   50.91        |   _$(Const("op =",_)$_$_) => r RS eq_reflection
   50.92        |   _$(Const("not",_)$_) => r RS not_P_imp_P_eq_False
   50.93        |   _ => r RS P_imp_P_eq_True;
   50.94 @@ -153,8 +153,8 @@
   50.95  val expand_if = prove_goal HOL.thy
   50.96      "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))"
   50.97   (fn _=> [ (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1),
   50.98 -         rtac (if_P RS ssubst) 2,
   50.99 -         rtac (if_not_P RS ssubst) 1,
  50.100 +         stac if_P 2,
  50.101 +         stac if_not_P 1,
  50.102           REPEAT(fast_tac HOL_cs 1) ]);
  50.103  
  50.104  val if_bool_eq = prove_goal HOL.thy
  50.105 @@ -183,21 +183,21 @@
  50.106  
  50.107  (*Miniscoping: pushing in existential quantifiers*)
  50.108  val ex_simps = map prover 
  50.109 -		["(EX x. P x & Q)   = ((EX x.P x) & Q)",
  50.110 -		 "(EX x. P & Q x)   = (P & (EX x.Q x))",
  50.111 -		 "(EX x. P x | Q)   = ((EX x.P x) | Q)",
  50.112 -		 "(EX x. P | Q x)   = (P | (EX x.Q x))",
  50.113 -		 "(EX x. P x --> Q) = ((ALL x.P x) --> Q)",
  50.114 -		 "(EX x. P --> Q x) = (P --> (EX x.Q x))"];
  50.115 +                ["(EX x. P x & Q)   = ((EX x.P x) & Q)",
  50.116 +                 "(EX x. P & Q x)   = (P & (EX x.Q x))",
  50.117 +                 "(EX x. P x | Q)   = ((EX x.P x) | Q)",
  50.118 +                 "(EX x. P | Q x)   = (P | (EX x.Q x))",
  50.119 +                 "(EX x. P x --> Q) = ((ALL x.P x) --> Q)",
  50.120 +                 "(EX x. P --> Q x) = (P --> (EX x.Q x))"];
  50.121  
  50.122  (*Miniscoping: pushing in universal quantifiers*)
  50.123  val all_simps = map prover
  50.124 -		["(ALL x. P x & Q)   = ((ALL x.P x) & Q)",
  50.125 -		 "(ALL x. P & Q x)   = (P & (ALL x.Q x))",
  50.126 -		 "(ALL x. P x | Q)   = ((ALL x.P x) | Q)",
  50.127 -		 "(ALL x. P | Q x)   = (P | (ALL x.Q x))",
  50.128 -		 "(ALL x. P x --> Q) = ((EX x.P x) --> Q)",
  50.129 -		 "(ALL x. P --> Q x) = (P --> (ALL x.Q x))"];
  50.130 +                ["(ALL x. P x & Q)   = ((ALL x.P x) & Q)",
  50.131 +                 "(ALL x. P & Q x)   = (P & (ALL x.Q x))",
  50.132 +                 "(ALL x. P x | Q)   = ((ALL x.P x) | Q)",
  50.133 +                 "(ALL x. P | Q x)   = (P | (ALL x.Q x))",
  50.134 +                 "(ALL x. P x --> Q) = ((EX x.P x) --> Q)",
  50.135 +                 "(ALL x. P --> Q x) = (P --> (ALL x.Q x))"];
  50.136  
  50.137  val HOL_ss = empty_ss
  50.138        setmksimps (mksimps mksimps_pairs)
  50.139 @@ -205,7 +205,7 @@
  50.140                               ORELSE' etac FalseE)
  50.141        setsubgoaler asm_simp_tac
  50.142        addsimps ([if_True, if_False, o_apply, imp_disj, conj_assoc, disj_assoc,
  50.143 -		 cases_simp]
  50.144 +                 cases_simp]
  50.145          @ ex_simps @ all_simps @ simp_thms)
  50.146        addcongs [imp_cong];
  50.147  
  50.148 @@ -245,13 +245,13 @@
  50.149  val conj_cong = 
  50.150    let val th = prove_goal HOL.thy 
  50.151                  "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))"
  50.152 -		(fn _=> [fast_tac HOL_cs 1])
  50.153 +                (fn _=> [fast_tac HOL_cs 1])
  50.154    in  standard (impI RSN (2, th RS mp RS mp))  end;
  50.155  
  50.156  val rev_conj_cong =
  50.157    let val th = prove_goal HOL.thy 
  50.158                  "(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))"
  50.159 -		(fn _=> [fast_tac HOL_cs 1])
  50.160 +                (fn _=> [fast_tac HOL_cs 1])
  50.161    in  standard (impI RSN (2, th RS mp RS mp))  end;
  50.162  
  50.163  (* '|' congruence rule: not included by default! *)
  50.164 @@ -259,7 +259,7 @@
  50.165  val disj_cong = 
  50.166    let val th = prove_goal HOL.thy 
  50.167                  "(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))"
  50.168 -		(fn _=> [fast_tac HOL_cs 1])
  50.169 +                (fn _=> [fast_tac HOL_cs 1])
  50.170    in  standard (impI RSN (2, th RS mp RS mp))  end;
  50.171  
  50.172  (** 'if' congruence rules: neither included by default! *)