Ran expandshort
authorpaulson
Wed Apr 23 11:02:19 1997 +0200 (1997-04-23)
changeset 3018e65b60b28341
parent 3017 84c2178db936
child 3019 ca5a7bbbee6c
Ran expandshort
src/HOL/Integ/Group.ML
src/HOL/Integ/IntRing.ML
src/HOL/Integ/Ring.ML
src/HOL/MiniML/Generalize.ML
src/HOL/MiniML/Instance.ML
src/HOL/MiniML/MiniML.ML
src/HOL/MiniML/Type.ML
src/HOL/MiniML/W.ML
src/HOL/W0/W.ML
src/HOL/ex/LFilter.ML
src/HOL/ex/LList.ML
src/HOLCF/Discrete0.ML
src/HOLCF/Discrete1.ML
src/HOLCF/Porder.ML
src/HOLCF/ex/Focus_ex.ML
     1.1 --- a/src/HOL/Integ/Group.ML	Wed Apr 23 11:00:48 1997 +0200
     1.2 +++ b/src/HOL/Integ/Group.ML	Wed Apr 23 11:02:19 1997 +0200
     1.3 @@ -9,78 +9,78 @@
     1.4  Addsimps [zeroL,zeroR,plus_assoc,plus_commute];
     1.5  
     1.6  goal Group.thy "!!x::'a::add_group. (zero-x)+(x+y) = y";
     1.7 -br trans 1;
     1.8 -br (plus_assoc RS sym) 1;
     1.9 -by(stac left_inv 1);
    1.10 -br zeroL 1;
    1.11 +by (rtac trans 1);
    1.12 +by (rtac (plus_assoc RS sym) 1);
    1.13 +by (stac left_inv 1);
    1.14 +by (rtac zeroL 1);
    1.15  qed "left_inv2";
    1.16  
    1.17  goal Group.thy "!!x::'a::add_group. (zero-(zero-x)) = x";
    1.18 -br trans 1;
    1.19 -by(res_inst_tac [("x","zero-x")] left_inv2 2);
    1.20 -by(stac left_inv 1);
    1.21 -br (zeroR RS sym) 1;
    1.22 +by (rtac trans 1);
    1.23 +by (res_inst_tac [("x","zero-x")] left_inv2 2);
    1.24 +by (stac left_inv 1);
    1.25 +by (rtac (zeroR RS sym) 1);
    1.26  qed "inv_inv";
    1.27  
    1.28  goal Group.thy "zero-zero = (zero::'a::add_group)";
    1.29 -br trans 1;
    1.30 -br (zeroR RS sym) 1;
    1.31 -br trans 1;
    1.32 -by(res_inst_tac [("x","zero")] left_inv2 2);
    1.33 -by(Simp_tac 1);
    1.34 +by (rtac trans 1);
    1.35 +by (rtac (zeroR RS sym) 1);
    1.36 +by (rtac trans 1);
    1.37 +by (res_inst_tac [("x","zero")] left_inv2 2);
    1.38 +by (Simp_tac 1);
    1.39  qed "inv_zero";
    1.40  
    1.41  goal Group.thy "!!x::'a::add_group. x+(zero-x) = zero";
    1.42 -br trans 1;
    1.43 -by(res_inst_tac [("x","zero-x")] left_inv 2);
    1.44 -by(stac inv_inv 1);
    1.45 -br refl 1;
    1.46 +by (rtac trans 1);
    1.47 +by (res_inst_tac [("x","zero-x")] left_inv 2);
    1.48 +by (stac inv_inv 1);
    1.49 +by (rtac refl 1);
    1.50  qed "right_inv";
    1.51  
    1.52  goal Group.thy "!!x::'a::add_group. x+((zero-x)+y) = y";
    1.53 -br trans 1;
    1.54 -by(res_inst_tac [("x","zero-x")] left_inv2 2);
    1.55 -by(stac inv_inv 1);
    1.56 -br refl 1;
    1.57 +by (rtac trans 1);
    1.58 +by (res_inst_tac [("x","zero-x")] left_inv2 2);
    1.59 +by (stac inv_inv 1);
    1.60 +by (rtac refl 1);
    1.61  qed "right_inv2";
    1.62  
    1.63  goal Group.thy "!!x::'a::add_group. x-x = zero";
    1.64 -by(stac minus_inv 1);
    1.65 -br right_inv 1;
    1.66 +by (stac minus_inv 1);
    1.67 +by (rtac right_inv 1);
    1.68  qed "minus_self_zero";
    1.69  Addsimps [minus_self_zero];
    1.70  
    1.71  goal Group.thy "!!x::'a::add_group. x-zero = x";
    1.72 -by(stac minus_inv 1);
    1.73 -by(stac inv_zero 1);
    1.74 -br zeroR 1;
    1.75 +by (stac minus_inv 1);
    1.76 +by (stac inv_zero 1);
    1.77 +by (rtac zeroR 1);
    1.78  qed "minus_zero";
    1.79  Addsimps [minus_zero];
    1.80  
    1.81  val plus_cong = read_instantiate [("f1","op +")] (arg_cong RS cong);
    1.82  
    1.83  goal Group.thy "!!x::'a::add_group. zero-(x+y) = (zero-y)+(zero-x)";
    1.84 -br trans 1;
    1.85 - br zeroR 2;
    1.86 -br trans 1;
    1.87 - br plus_cong 2;
    1.88 -  br refl 2;
    1.89 - by(res_inst_tac [("x","x+y")] right_inv 2);
    1.90 -br trans 1;
    1.91 - br plus_assoc 2;
    1.92 -br trans 1;
    1.93 - br plus_cong 2;
    1.94 -  by(simp_tac (!simpset addsimps [left_inv,left_inv2,right_inv,right_inv2]) 2);
    1.95 - br refl 2;
    1.96 -br (zeroL RS sym) 1;
    1.97 +by (rtac trans 1);
    1.98 + by (rtac zeroR 2);
    1.99 +by (rtac trans 1);
   1.100 + by (rtac plus_cong 2);
   1.101 +  by (rtac refl 2);
   1.102 + by (res_inst_tac [("x","x+y")] right_inv 2);
   1.103 +by (rtac trans 1);
   1.104 + by (rtac plus_assoc 2);
   1.105 +by (rtac trans 1);
   1.106 + by (rtac plus_cong 2);
   1.107 +  by (simp_tac (!simpset addsimps [left_inv,left_inv2,right_inv,right_inv2]) 2);
   1.108 + by (rtac refl 2);
   1.109 +by (rtac (zeroL RS sym) 1);
   1.110  qed "inv_plus";
   1.111  
   1.112  goal Group.thy "x+(y+z)=y+(x+z::'a::add_agroup)";
   1.113 -br trans 1;
   1.114 -br plus_commute 1;
   1.115 -br trans 1;
   1.116 -br plus_assoc 1;
   1.117 -by(Simp_tac 1);
   1.118 +by (rtac trans 1);
   1.119 +by (rtac plus_commute 1);
   1.120 +by (rtac trans 1);
   1.121 +by (rtac plus_assoc 1);
   1.122 +by (Simp_tac 1);
   1.123  qed "plus_commuteL";
   1.124  Addsimps [plus_commuteL];
   1.125  
   1.126 @@ -89,39 +89,39 @@
   1.127  (* Phase 1 *)
   1.128  
   1.129  goal Group.thy "!!x::'a::add_agroup. (x+(zero-y))+z = (x+z)+(zero-y)";
   1.130 -by(Simp_tac 1);
   1.131 +by (Simp_tac 1);
   1.132  val lemma = result();
   1.133  bind_thm("plus_minusL",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
   1.134  
   1.135  goal Group.thy "!!x::'a::add_agroup. x+(zero-(y+z)) = (x+(zero-y))+(zero-z)";
   1.136 -by(Simp_tac 1);
   1.137 +by (Simp_tac 1);
   1.138  val lemma = result();
   1.139  bind_thm("minus_plusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
   1.140  
   1.141  goal Group.thy "!!x::'a::add_agroup. x+(zero-(y+(zero-z))) = (x+z)+(zero-y)";
   1.142 -by(Simp_tac 1);
   1.143 +by (Simp_tac 1);
   1.144  val lemma = result();
   1.145  bind_thm("minus_minusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
   1.146  
   1.147  goal Group.thy "!!x::'a::add_agroup. x+(y+(zero-z)) = (x+y)+(zero-z)";
   1.148 -by(Simp_tac 1);
   1.149 +by (Simp_tac 1);
   1.150  val lemma = result();
   1.151  bind_thm("plus_minusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
   1.152  
   1.153  (* Phase 2 *)
   1.154  
   1.155  goal Group.thy "!!x::'a::add_agroup. (x+y)+(zero-z) = x+(y+(zero-z))";
   1.156 -by(Simp_tac 1);
   1.157 +by (Simp_tac 1);
   1.158  val lemma = result();
   1.159  bind_thm("minus_plusL2",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
   1.160  
   1.161  goal Group.thy "!!x::'a::add_agroup. (x+y)+(zero-x) = y";
   1.162 -br (plus_assoc RS trans) 1;
   1.163 -br trans 1;
   1.164 - br plus_cong 1;
   1.165 -  br refl 1;
   1.166 - br right_inv2 2;
   1.167 -br plus_commute 1;
   1.168 +by (rtac (plus_assoc RS trans) 1);
   1.169 +by (rtac trans 1);
   1.170 + by (rtac plus_cong 1);
   1.171 +  by (rtac refl 1);
   1.172 + by (rtac right_inv2 2);
   1.173 +by (rtac plus_commute 1);
   1.174  val lemma = result();
   1.175  bind_thm("minus_plusL3",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
   1.176  
     2.1 --- a/src/HOL/Integ/IntRing.ML	Wed Apr 23 11:00:48 1997 +0200
     2.2 +++ b/src/HOL/Integ/IntRing.ML	Wed Apr 23 11:02:19 1997 +0200
     2.3 @@ -14,5 +14,5 @@
     2.4  \  sq(i1*j2 + i2*j1 + i3*j4 - i4*j3)  + \
     2.5  \  sq(i1*j3 - i2*j4 + i3*j1 + i4*j2)  + \
     2.6  \  sq(i1*j4 + i2*j3 - i3*j2 + i4*j1)";
     2.7 -br Lagrange_lemma 1;
     2.8 +by (rtac Lagrange_lemma 1);
     2.9  qed "Lagrange_lemma_int";
     3.1 --- a/src/HOL/Integ/Ring.ML	Wed Apr 23 11:00:48 1997 +0200
     3.2 +++ b/src/HOL/Integ/Ring.ML	Wed Apr 23 11:02:19 1997 +0200
     3.3 @@ -17,123 +17,123 @@
     3.4  Addsimps [times_assoc,times_commute,distribL,distribR];
     3.5  
     3.6  goal Ring.thy "!!x::'a::cring. x*(y*z)=y*(x*z)";
     3.7 -br trans 1;
     3.8 -br times_commute 1;
     3.9 -br trans 1;
    3.10 -br times_assoc 1;
    3.11 -by(Simp_tac 1);
    3.12 +by (rtac trans 1);
    3.13 +by (rtac times_commute 1);
    3.14 +by (rtac trans 1);
    3.15 +by (rtac times_assoc 1);
    3.16 +by (Simp_tac 1);
    3.17  qed "times_commuteL";
    3.18  Addsimps [times_commuteL];
    3.19  
    3.20  val times_cong = read_instantiate [("f1","op *")] (arg_cong RS cong);
    3.21  
    3.22  goal Ring.thy "!!x::'a::ring. zero*x = zero";
    3.23 -br trans 1;
    3.24 - br right_inv 2;
    3.25 -br trans 1;
    3.26 - br plus_cong 2;
    3.27 -  br refl 3;
    3.28 - br trans 2;
    3.29 -  br times_cong 3;
    3.30 -   br zeroL 3;
    3.31 -  br refl 3;
    3.32 - br (distribR RS sym) 2;
    3.33 -br trans 1;
    3.34 +by (rtac trans 1);
    3.35 + by (rtac right_inv 2);
    3.36 +by (rtac trans 1);
    3.37 + by (rtac plus_cong 2);
    3.38 +  by (rtac refl 3);
    3.39 + by (rtac trans 2);
    3.40 +  by (rtac times_cong 3);
    3.41 +   by (rtac zeroL 3);
    3.42 +  by (rtac refl 3);
    3.43 + by (rtac (distribR RS sym) 2);
    3.44 +by (rtac trans 1);
    3.45   br(plus_assoc RS sym) 2;
    3.46 -br trans 1;
    3.47 - br plus_cong 2;
    3.48 -  br refl 2;
    3.49 - br (right_inv RS sym) 2;
    3.50 -br (zeroR RS sym) 1;
    3.51 +by (rtac trans 1);
    3.52 + by (rtac plus_cong 2);
    3.53 +  by (rtac refl 2);
    3.54 + by (rtac (right_inv RS sym) 2);
    3.55 +by (rtac (zeroR RS sym) 1);
    3.56  qed "mult_zeroL";
    3.57  
    3.58  goal Ring.thy "!!x::'a::ring. x*zero = zero";
    3.59 -br trans 1;
    3.60 - br right_inv 2;
    3.61 -br trans 1;
    3.62 - br plus_cong 2;
    3.63 -  br refl 3;
    3.64 - br trans 2;
    3.65 -  br times_cong 3;
    3.66 -   br zeroL 4;
    3.67 -  br refl 3;
    3.68 - br (distribL RS sym) 2;
    3.69 -br trans 1;
    3.70 +by (rtac trans 1);
    3.71 + by (rtac right_inv 2);
    3.72 +by (rtac trans 1);
    3.73 + by (rtac plus_cong 2);
    3.74 +  by (rtac refl 3);
    3.75 + by (rtac trans 2);
    3.76 +  by (rtac times_cong 3);
    3.77 +   by (rtac zeroL 4);
    3.78 +  by (rtac refl 3);
    3.79 + by (rtac (distribL RS sym) 2);
    3.80 +by (rtac trans 1);
    3.81   br(plus_assoc RS sym) 2;
    3.82 -br trans 1;
    3.83 - br plus_cong 2;
    3.84 -  br refl 2;
    3.85 - br (right_inv RS sym) 2;
    3.86 -br (zeroR RS sym) 1;
    3.87 +by (rtac trans 1);
    3.88 + by (rtac plus_cong 2);
    3.89 +  by (rtac refl 2);
    3.90 + by (rtac (right_inv RS sym) 2);
    3.91 +by (rtac (zeroR RS sym) 1);
    3.92  qed "mult_zeroR";
    3.93  
    3.94  goal Ring.thy "!!x::'a::ring. (zero-x)*y = zero-(x*y)";
    3.95 -br trans 1;
    3.96 - br zeroL 2;
    3.97 -br trans 1;
    3.98 - br plus_cong 2;
    3.99 -  br refl 3;
   3.100 - br mult_zeroL 2;
   3.101 -br trans 1;
   3.102 - br plus_cong 2;
   3.103 -  br refl 3;
   3.104 - br times_cong 2;
   3.105 -  br left_inv 2;
   3.106 - br refl 2;
   3.107 -br trans 1;
   3.108 - br plus_cong 2;
   3.109 -  br refl 3;
   3.110 - br (distribR RS sym) 2;
   3.111 -br trans 1;
   3.112 +by (rtac trans 1);
   3.113 + by (rtac zeroL 2);
   3.114 +by (rtac trans 1);
   3.115 + by (rtac plus_cong 2);
   3.116 +  by (rtac refl 3);
   3.117 + by (rtac mult_zeroL 2);
   3.118 +by (rtac trans 1);
   3.119 + by (rtac plus_cong 2);
   3.120 +  by (rtac refl 3);
   3.121 + by (rtac times_cong 2);
   3.122 +  by (rtac left_inv 2);
   3.123 + by (rtac refl 2);
   3.124 +by (rtac trans 1);
   3.125 + by (rtac plus_cong 2);
   3.126 +  by (rtac refl 3);
   3.127 + by (rtac (distribR RS sym) 2);
   3.128 +by (rtac trans 1);
   3.129   br(plus_assoc RS sym) 2;
   3.130 -br trans 1;
   3.131 - br plus_cong 2;
   3.132 -  br refl 2;
   3.133 - br (right_inv RS sym) 2;
   3.134 -br (zeroR RS sym) 1;
   3.135 +by (rtac trans 1);
   3.136 + by (rtac plus_cong 2);
   3.137 +  by (rtac refl 2);
   3.138 + by (rtac (right_inv RS sym) 2);
   3.139 +by (rtac (zeroR RS sym) 1);
   3.140  qed "mult_invL";
   3.141  
   3.142  goal Ring.thy "!!x::'a::ring. x*(zero-y) = zero-(x*y)";
   3.143 -br trans 1;
   3.144 - br zeroL 2;
   3.145 -br trans 1;
   3.146 - br plus_cong 2;
   3.147 -  br refl 3;
   3.148 - br mult_zeroR 2;
   3.149 -br trans 1;
   3.150 - br plus_cong 2;
   3.151 -  br refl 3;
   3.152 - br times_cong 2;
   3.153 -  br refl 2;
   3.154 - br left_inv 2;
   3.155 -br trans 1;
   3.156 - br plus_cong 2;
   3.157 -  br refl 3;
   3.158 - br (distribL RS sym) 2;
   3.159 -br trans 1;
   3.160 +by (rtac trans 1);
   3.161 + by (rtac zeroL 2);
   3.162 +by (rtac trans 1);
   3.163 + by (rtac plus_cong 2);
   3.164 +  by (rtac refl 3);
   3.165 + by (rtac mult_zeroR 2);
   3.166 +by (rtac trans 1);
   3.167 + by (rtac plus_cong 2);
   3.168 +  by (rtac refl 3);
   3.169 + by (rtac times_cong 2);
   3.170 +  by (rtac refl 2);
   3.171 + by (rtac left_inv 2);
   3.172 +by (rtac trans 1);
   3.173 + by (rtac plus_cong 2);
   3.174 +  by (rtac refl 3);
   3.175 + by (rtac (distribL RS sym) 2);
   3.176 +by (rtac trans 1);
   3.177   br(plus_assoc RS sym) 2;
   3.178 -br trans 1;
   3.179 - br plus_cong 2;
   3.180 -  br refl 2;
   3.181 - br (right_inv RS sym) 2;
   3.182 -br (zeroR RS sym) 1;
   3.183 +by (rtac trans 1);
   3.184 + by (rtac plus_cong 2);
   3.185 +  by (rtac refl 2);
   3.186 + by (rtac (right_inv RS sym) 2);
   3.187 +by (rtac (zeroR RS sym) 1);
   3.188  qed "mult_invR";
   3.189  
   3.190  Addsimps[mult_invL,mult_invR];
   3.191  
   3.192  
   3.193  goal Ring.thy "!!x::'a::ring. x*(y-z) = x*y - x*z";
   3.194 -by(stac minus_inv 1);
   3.195 -br sym 1;
   3.196 -by(stac minus_inv 1);
   3.197 -by(Simp_tac 1);
   3.198 +by (stac minus_inv 1);
   3.199 +by (rtac sym 1);
   3.200 +by (stac minus_inv 1);
   3.201 +by (Simp_tac 1);
   3.202  qed "minus_distribL";
   3.203  
   3.204  goal Ring.thy "!!x::'a::ring. (x-y)*z = x*z - y*z";
   3.205 -by(stac minus_inv 1);
   3.206 -br sym 1;
   3.207 -by(stac minus_inv 1);
   3.208 -by(Simp_tac 1);
   3.209 +by (stac minus_inv 1);
   3.210 +by (rtac sym 1);
   3.211 +by (stac minus_inv 1);
   3.212 +by (Simp_tac 1);
   3.213  qed "minus_distribR";
   3.214  
   3.215  Addsimps [minus_distribL,minus_distribR];
     4.1 --- a/src/HOL/MiniML/Generalize.ML	Wed Apr 23 11:00:48 1997 +0200
     4.2 +++ b/src/HOL/MiniML/Generalize.ML	Wed Apr 23 11:02:19 1997 +0200
     4.3 @@ -87,31 +87,31 @@
     4.4  qed_spec_mp "gen_subst_commutes";
     4.5  
     4.6  goal Generalize.thy "free_tv(t::typ) <= free_tv(A) --> bound_typ_inst S (gen A t) = t";
     4.7 -by(typ.induct_tac "t" 1);
     4.8 -by(ALLGOALS Asm_simp_tac);
     4.9 -by(Fast_tac 1);
    4.10 +by (typ.induct_tac "t" 1);
    4.11 +by (ALLGOALS Asm_simp_tac);
    4.12 +by (Fast_tac 1);
    4.13  qed_spec_mp "bound_typ_inst_gen";
    4.14  Addsimps [bound_typ_inst_gen];
    4.15  
    4.16  goalw Generalize.thy [le_type_scheme_def,is_bound_typ_instance]
    4.17    "gen ($ S A) ($ S t) <= $ S (gen A t)";
    4.18 -by(safe_tac (!claset));
    4.19 -by(rename_tac "R" 1);
    4.20 -by(res_inst_tac [("x", "(%a. bound_typ_inst R (gen ($S A) (S a)))")] exI 1);
    4.21 -by(typ.induct_tac "t" 1);
    4.22 - by(simp_tac (!simpset setloop (split_tac[expand_if])) 1);
    4.23 -by(Asm_simp_tac 1);
    4.24 +by (safe_tac (!claset));
    4.25 +by (rename_tac "R" 1);
    4.26 +by (res_inst_tac [("x", "(%a. bound_typ_inst R (gen ($S A) (S a)))")] exI 1);
    4.27 +by (typ.induct_tac "t" 1);
    4.28 + by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
    4.29 +by (Asm_simp_tac 1);
    4.30  qed "gen_bound_typ_instance";
    4.31  
    4.32  goalw Generalize.thy [le_type_scheme_def,is_bound_typ_instance]
    4.33    "!!A B. free_tv B <= free_tv A ==> gen A t <= gen B t";
    4.34 -by(safe_tac (!claset));
    4.35 -by(rename_tac "S" 1);
    4.36 -by(res_inst_tac [("x","%b. if b:free_tv A then TVar b else S b")] exI 1);
    4.37 +by (safe_tac (!claset));
    4.38 +by (rename_tac "S" 1);
    4.39 +by (res_inst_tac [("x","%b. if b:free_tv A then TVar b else S b")] exI 1);
    4.40  by (typ.induct_tac "t" 1);
    4.41 - by(asm_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
    4.42 - by(Fast_tac 1);
    4.43 -by(Asm_simp_tac 1);
    4.44 + by (asm_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
    4.45 + by (Fast_tac 1);
    4.46 +by (Asm_simp_tac 1);
    4.47  qed "free_tv_subset_gen_le";
    4.48  
    4.49  goalw thy [le_type_scheme_def,is_bound_typ_instance] 
    4.50 @@ -127,7 +127,7 @@
    4.51  by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    4.52  by (subgoal_tac "n <= n + nat" 1);
    4.53  by (forw_inst_tac [("t","A")] new_tv_le 1);
    4.54 -ba 1;
    4.55 +by (assume_tac 1);
    4.56  by (dtac new_tv_not_free_tv 1);
    4.57  by (dtac new_tv_not_free_tv 1);
    4.58  by (asm_simp_tac (!simpset addsimps [diff_add_inverse]) 1);
     5.1 --- a/src/HOL/MiniML/Instance.ML	Wed Apr 23 11:00:48 1997 +0200
     5.2 +++ b/src/HOL/MiniML/Instance.ML	Wed Apr 23 11:02:19 1997 +0200
     5.3 @@ -70,7 +70,7 @@
     5.4  by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
     5.5  by (strip_tac 1);
     5.6  by (dres_inst_tac [("x","x")] bspec 1);
     5.7 -ba 1;
     5.8 +by (assume_tac 1);
     5.9  by (dres_inst_tac [("x","x")] bspec 1);
    5.10  by (Asm_simp_tac 1);
    5.11  by (Asm_full_simp_tac 1);
    5.12 @@ -110,7 +110,7 @@
    5.13  by (cut_inst_tac [("sch","sch")] fresh_variable_type_schemes 1); 
    5.14  by (cut_inst_tac [("sch","sch'")] fresh_variable_type_schemes 1);
    5.15  by (dtac make_one_new_out_of_two 1);
    5.16 -ba 1;
    5.17 +by (assume_tac 1);
    5.18  by (thin_tac "? n. new_tv n sch'" 1); 
    5.19  by (etac exE 1);
    5.20  by (etac allE 1);
    5.21 @@ -142,7 +142,7 @@
    5.22  by (Asm_full_simp_tac 1);
    5.23  by (rotate_tac 1 1);
    5.24  by (rtac mp 1);
    5.25 -ba 2;
    5.26 +by (assume_tac 2);
    5.27  by (type_scheme.induct_tac "sch" 1);
    5.28  by (Simp_tac 1);
    5.29  by (Asm_full_simp_tac 1);
    5.30 @@ -160,18 +160,18 @@
    5.31  
    5.32  goalw thy [le_env_def]
    5.33    "(sch # A <= sch' # B) = (sch <= (sch'::type_scheme) & A <= B)";
    5.34 -by(Simp_tac 1);
    5.35 -br iffI 1;
    5.36 - by(SELECT_GOAL(safe_tac (!claset))1);
    5.37 -  by(eres_inst_tac [("x","0")] allE 1);
    5.38 -  by(Asm_full_simp_tac 1);
    5.39 - by(eres_inst_tac [("x","Suc i")] allE 1);
    5.40 - by(Asm_full_simp_tac 1);
    5.41 -br conjI 1;
    5.42 - by(Fast_tac 1);
    5.43 -br allI 1;
    5.44 -by(nat_ind_tac "i" 1);
    5.45 -by(ALLGOALS Asm_simp_tac);
    5.46 +by (Simp_tac 1);
    5.47 +by (rtac iffI 1);
    5.48 + by (SELECT_GOAL(safe_tac (!claset))1);
    5.49 +  by (eres_inst_tac [("x","0")] allE 1);
    5.50 +  by (Asm_full_simp_tac 1);
    5.51 + by (eres_inst_tac [("x","Suc i")] allE 1);
    5.52 + by (Asm_full_simp_tac 1);
    5.53 +by (rtac conjI 1);
    5.54 + by (Fast_tac 1);
    5.55 +by (rtac allI 1);
    5.56 +by (nat_ind_tac "i" 1);
    5.57 +by (ALLGOALS Asm_simp_tac);
    5.58  qed "le_env_Cons";
    5.59  AddIffs [le_env_Cons];
    5.60  
    5.61 @@ -196,59 +196,59 @@
    5.62  qed "S_compatible_le_scheme_lists";
    5.63  
    5.64  goalw thy [le_type_scheme_def] "!!t.[| t <| sch; sch <= sch' |] ==> t <| sch'";
    5.65 -by(Fast_tac 1);
    5.66 +by (Fast_tac 1);
    5.67  qed "bound_typ_instance_trans";
    5.68  
    5.69  goalw thy [le_type_scheme_def] "sch <= (sch::type_scheme)";
    5.70 -by(Fast_tac 1);
    5.71 +by (Fast_tac 1);
    5.72  qed "le_type_scheme_refl";
    5.73  AddIffs [le_type_scheme_refl];
    5.74  
    5.75  goalw thy [le_env_def] "A <= (A::type_scheme list)";
    5.76 -by(Fast_tac 1);
    5.77 +by (Fast_tac 1);
    5.78  qed "le_env_refl";
    5.79  AddIffs [le_env_refl];
    5.80  
    5.81  goalw thy [le_type_scheme_def,is_bound_typ_instance] "sch <= BVar n";
    5.82 -by(strip_tac 1);
    5.83 -by(res_inst_tac [("x","%a.t")]exI 1);
    5.84 -by(Simp_tac 1);
    5.85 +by (strip_tac 1);
    5.86 +by (res_inst_tac [("x","%a.t")]exI 1);
    5.87 +by (Simp_tac 1);
    5.88  qed "bound_typ_instance_BVar";
    5.89  AddIffs [bound_typ_instance_BVar];
    5.90  
    5.91  goalw thy [le_type_scheme_def,is_bound_typ_instance] "(sch <= FVar n) = (sch = FVar n)";
    5.92 -by(type_scheme.induct_tac "sch" 1);
    5.93 -  by(Simp_tac 1);
    5.94 - by(Simp_tac 1);
    5.95 - by(SELECT_GOAL(safe_tac(!claset))1);
    5.96 - by(eres_inst_tac [("x","TVar n -> TVar n")] allE 1);
    5.97 - by(Asm_full_simp_tac 1);
    5.98 - by(Fast_tac 1);
    5.99 -by(Asm_full_simp_tac 1);
   5.100 -br iffI 1;
   5.101 - by(eres_inst_tac [("x","bound_typ_inst S type_scheme1 -> bound_typ_inst S type_scheme2")] allE 1);
   5.102 - by(Asm_full_simp_tac 1);
   5.103 - by(Fast_tac 1);
   5.104 -by(Fast_tac 1);
   5.105 +by (type_scheme.induct_tac "sch" 1);
   5.106 +  by (Simp_tac 1);
   5.107 + by (Simp_tac 1);
   5.108 + by (SELECT_GOAL(safe_tac(!claset))1);
   5.109 + by (eres_inst_tac [("x","TVar n -> TVar n")] allE 1);
   5.110 + by (Asm_full_simp_tac 1);
   5.111 + by (Fast_tac 1);
   5.112 +by (Asm_full_simp_tac 1);
   5.113 +by (rtac iffI 1);
   5.114 + by (eres_inst_tac [("x","bound_typ_inst S type_scheme1 -> bound_typ_inst S type_scheme2")] allE 1);
   5.115 + by (Asm_full_simp_tac 1);
   5.116 + by (Fast_tac 1);
   5.117 +by (Fast_tac 1);
   5.118  qed "le_FVar";
   5.119  Addsimps [le_FVar];
   5.120  
   5.121  goalw thy [le_type_scheme_def,is_bound_typ_instance] "~(FVar n <= sch1 =-> sch2)";
   5.122 -by(Simp_tac 1);
   5.123 +by (Simp_tac 1);
   5.124  qed "not_FVar_le_Fun";
   5.125  AddIffs [not_FVar_le_Fun];
   5.126  
   5.127  goalw thy [le_type_scheme_def,is_bound_typ_instance] "~(BVar n <= sch1 =-> sch2)";
   5.128 -by(Simp_tac 1);
   5.129 -by(res_inst_tac [("x","TVar n")] exI 1);
   5.130 -by(Simp_tac 1);
   5.131 -by(Fast_tac 1);
   5.132 +by (Simp_tac 1);
   5.133 +by (res_inst_tac [("x","TVar n")] exI 1);
   5.134 +by (Simp_tac 1);
   5.135 +by (Fast_tac 1);
   5.136  qed "not_BVar_le_Fun";
   5.137  AddIffs [not_BVar_le_Fun];
   5.138  
   5.139  goalw thy [le_type_scheme_def,is_bound_typ_instance]
   5.140    "!!sch1. (sch1 =-> sch2 <= sch1' =-> sch2') ==> sch1 <= sch1' & sch2 <= sch2'";
   5.141 -by(fast_tac (!claset addss !simpset) 1);
   5.142 +by (fast_tac (!claset addss !simpset) 1);
   5.143  qed "Fun_le_FunD";
   5.144  
   5.145  goal thy "(sch' <= sch1 =-> sch2) --> (? sch'1 sch'2. sch' = sch'1 =-> sch'2)";
   5.146 @@ -259,33 +259,33 @@
   5.147  qed_spec_mp "scheme_le_Fun";
   5.148  
   5.149  goal thy "!sch'::type_scheme. sch <= sch' --> free_tv sch' <= free_tv sch";
   5.150 -by(type_scheme.induct_tac "sch" 1);
   5.151 -  br allI 1;
   5.152 -  by(type_scheme.induct_tac "sch'" 1);
   5.153 -    by(Simp_tac 1);
   5.154 -   by(Simp_tac 1);
   5.155 -  by(Simp_tac 1);
   5.156 - br allI 1;
   5.157 - by(type_scheme.induct_tac "sch'" 1);
   5.158 -   by(Simp_tac 1);
   5.159 -  by(Simp_tac 1);
   5.160 - by(Simp_tac 1);
   5.161 -br allI 1;
   5.162 -by(type_scheme.induct_tac "sch'" 1);
   5.163 -  by(Simp_tac 1);
   5.164 - by(Simp_tac 1);
   5.165 -by(Asm_full_simp_tac 1);
   5.166 -by(strip_tac 1);
   5.167 -bd Fun_le_FunD 1;
   5.168 -by(Fast_tac 1);
   5.169 +by (type_scheme.induct_tac "sch" 1);
   5.170 +  by (rtac allI 1);
   5.171 +  by (type_scheme.induct_tac "sch'" 1);
   5.172 +    by (Simp_tac 1);
   5.173 +   by (Simp_tac 1);
   5.174 +  by (Simp_tac 1);
   5.175 + by (rtac allI 1);
   5.176 + by (type_scheme.induct_tac "sch'" 1);
   5.177 +   by (Simp_tac 1);
   5.178 +  by (Simp_tac 1);
   5.179 + by (Simp_tac 1);
   5.180 +by (rtac allI 1);
   5.181 +by (type_scheme.induct_tac "sch'" 1);
   5.182 +  by (Simp_tac 1);
   5.183 + by (Simp_tac 1);
   5.184 +by (Asm_full_simp_tac 1);
   5.185 +by (strip_tac 1);
   5.186 +by (dtac Fun_le_FunD 1);
   5.187 +by (Fast_tac 1);
   5.188  qed_spec_mp "le_type_scheme_free_tv";
   5.189  
   5.190  goal thy "!A::type_scheme list. A <= B --> free_tv B <= free_tv A";
   5.191 -by(list.induct_tac "B" 1);
   5.192 - by(Simp_tac 1);
   5.193 -br allI 1;
   5.194 -by(list.induct_tac "A" 1);
   5.195 - by(simp_tac (!simpset addsimps [le_env_def]) 1);
   5.196 -by(Simp_tac 1);
   5.197 -by(fast_tac (!claset addDs [le_type_scheme_free_tv]) 1);
   5.198 +by (list.induct_tac "B" 1);
   5.199 + by (Simp_tac 1);
   5.200 +by (rtac allI 1);
   5.201 +by (list.induct_tac "A" 1);
   5.202 + by (simp_tac (!simpset addsimps [le_env_def]) 1);
   5.203 +by (Simp_tac 1);
   5.204 +by (fast_tac (!claset addDs [le_type_scheme_free_tv]) 1);
   5.205  qed_spec_mp "le_env_free_tv";
     6.1 --- a/src/HOL/MiniML/MiniML.ML	Wed Apr 23 11:00:48 1997 +0200
     6.2 +++ b/src/HOL/MiniML/MiniML.ML	Wed Apr 23 11:02:19 1997 +0200
     6.3 @@ -128,7 +128,7 @@
     6.4  by (step_tac (!claset) 1);
     6.5  by (cut_facts_tac [aux_plus] 1);
     6.6  by (dtac new_tv_le 1);
     6.7 -ba 1;
     6.8 +by (assume_tac 1);
     6.9  by (rotate_tac 1 1);
    6.10  by (dtac new_tv_not_free_tv 1);
    6.11  by (Fast_tac 1);
    6.12 @@ -138,7 +138,7 @@
    6.13  by (step_tac (!claset) 1);
    6.14  by (cut_facts_tac [aux_plus] 1);
    6.15  by (dtac new_tv_le 1);
    6.16 -ba 1;
    6.17 +by (assume_tac 1);
    6.18  by (rotate_tac 1 1);
    6.19  by (dtac new_tv_not_free_tv 1);
    6.20  by (Fast_tac 1);
    6.21 @@ -164,7 +164,7 @@
    6.22  by (Asm_simp_tac 1);
    6.23  by (subgoal_tac "n <= n + nat" 1);
    6.24  by (dtac new_tv_le 1);
    6.25 -ba 1;
    6.26 +by (assume_tac 1);
    6.27  by (dtac new_tv_not_free_tv 1);
    6.28  by (dtac new_tv_not_free_tv 1);
    6.29  by (asm_simp_tac (!simpset addsimps [diff_add_inverse ]) 1);
    6.30 @@ -175,12 +175,12 @@
    6.31  AddSIs has_type.intrs;
    6.32  
    6.33  goal thy "!!e. A |- e::t ==> !B. A <= B -->  B |- e::t";
    6.34 -by(etac has_type.induct 1);
    6.35 -   by(simp_tac (!simpset addsimps [le_env_def]) 1);
    6.36 -   by(fast_tac (!claset addEs [bound_typ_instance_trans] addss !simpset) 1);
    6.37 -  by(Asm_full_simp_tac 1);
    6.38 - by(Fast_tac 1);
    6.39 -by(slow_tac (!claset addEs [le_env_free_tv RS free_tv_subset_gen_le]) 1);
    6.40 +by (etac has_type.induct 1);
    6.41 +   by (simp_tac (!simpset addsimps [le_env_def]) 1);
    6.42 +   by (fast_tac (!claset addEs [bound_typ_instance_trans] addss !simpset) 1);
    6.43 +  by (Asm_full_simp_tac 1);
    6.44 + by (Fast_tac 1);
    6.45 +by (slow_tac (!claset addEs [le_env_free_tv RS free_tv_subset_gen_le]) 1);
    6.46  qed_spec_mp "has_type_le_env";
    6.47  
    6.48  (* has_type is closed w.r.t. substitution *)
    6.49 @@ -220,7 +220,7 @@
    6.50   val o_apply = prove_goalw HOL.thy [o_def] "(f o g) x = f (g x)"
    6.51   (fn _ => [rtac refl 1]);
    6.52   by (stac (S'_A_eq_S'_alpha_A) 1);
    6.53 - ba 1;
    6.54 + by (assume_tac 1);
    6.55  by (stac S_o_alpha_typ 1);
    6.56  by (stac gen_subst_commutes 1);
    6.57   by (rtac subset_antisym 1);
    6.58 @@ -242,7 +242,7 @@
    6.59  by (rtac has_type_le_env 1);
    6.60   by (dtac spec 1);
    6.61   by (dtac spec 1);
    6.62 - ba 1;
    6.63 + by (assume_tac 1);
    6.64  by (rtac (app_subst_Cons RS subst) 1);
    6.65  by (rtac S_compatible_le_scheme_lists 1);
    6.66  by (Asm_simp_tac 1);
     7.1 --- a/src/HOL/MiniML/Type.ML	Wed Apr 23 11:00:48 1997 +0200
     7.2 +++ b/src/HOL/MiniML/Type.ML	Wed Apr 23 11:02:19 1997 +0200
     7.3 @@ -18,15 +18,15 @@
     7.4  
     7.5  goal thy "!t'.mk_scheme t = mk_scheme t' --> t=t'";
     7.6  by (typ.induct_tac "t" 1);
     7.7 - br allI 1;
     7.8 + by (rtac allI 1);
     7.9   by (typ.induct_tac "t'" 1);
    7.10 -  by(Simp_tac 1);
    7.11 - by(Asm_full_simp_tac 1);
    7.12 -br allI 1;
    7.13 +  by (Simp_tac 1);
    7.14 + by (Asm_full_simp_tac 1);
    7.15 +by (rtac allI 1);
    7.16  by (typ.induct_tac "t'" 1);
    7.17 - by(Simp_tac 1);
    7.18 -by(Asm_full_simp_tac 1);
    7.19 -by(Fast_tac 1);
    7.20 + by (Simp_tac 1);
    7.21 +by (Asm_full_simp_tac 1);
    7.22 +by (Fast_tac 1);
    7.23  qed_spec_mp "mk_scheme_injective";
    7.24  
    7.25  goal thy "!!t. free_tv (mk_scheme t) = free_tv t";
    7.26 @@ -105,21 +105,21 @@
    7.27  
    7.28  goalw thy [id_subst_def,new_tv_def,free_tv_subst,dom_def,cod_def]
    7.29    "new_tv n id_subst";
    7.30 -by(Simp_tac 1);
    7.31 +by (Simp_tac 1);
    7.32  qed "new_tv_id_subst";
    7.33  Addsimps[new_tv_id_subst];
    7.34  
    7.35  goal thy "new_tv n (sch::type_scheme) --> \
    7.36  \              $(%k.if k<n then S k else S' k) sch = $S sch";
    7.37  by (type_scheme.induct_tac "sch" 1);
    7.38 -by(ALLGOALS Asm_simp_tac);
    7.39 +by (ALLGOALS Asm_simp_tac);
    7.40  qed "new_if_subst_type_scheme";
    7.41  Addsimps [new_if_subst_type_scheme];
    7.42  
    7.43  goal thy "new_tv n (A::type_scheme list) --> \
    7.44  \              $(%k.if k<n then S k else S' k) A = $S A";
    7.45  by (list.induct_tac "A" 1);
    7.46 -by(ALLGOALS Asm_simp_tac);
    7.47 +by (ALLGOALS Asm_simp_tac);
    7.48  qed "new_if_subst_type_scheme_list";
    7.49  Addsimps [new_if_subst_type_scheme_list];
    7.50  
    7.51 @@ -253,17 +253,17 @@
    7.52  
    7.53  goalw thy [free_tv_subst] 
    7.54        "!!v. v : cod S ==> v : free_tv S";
    7.55 -by( fast_tac set_cs 1);
    7.56 +by ( fast_tac set_cs 1);
    7.57  qed "codD";
    7.58   
    7.59  goalw thy [free_tv_subst,dom_def] 
    7.60        "!! x. x ~: free_tv S ==> S x = TVar x";
    7.61 -by( fast_tac set_cs 1);
    7.62 +by ( fast_tac set_cs 1);
    7.63  qed "not_free_impl_id";
    7.64  
    7.65  goalw thy [new_tv_def] 
    7.66        "!! n. [| new_tv n t; m:free_tv t |] ==> m<n";
    7.67 -by( fast_tac HOL_cs 1 );
    7.68 +by ( fast_tac HOL_cs 1 );
    7.69  qed "free_tv_le_new_tv";
    7.70  
    7.71  goalw thy [dom_def,cod_def,UNION_def,Bex_def]
    7.72 @@ -278,26 +278,26 @@
    7.73  
    7.74  goal thy 
    7.75       "free_tv (S (v::nat)) <= cod S Un {v}";
    7.76 -by( cut_inst_tac [("P","v:dom S")] excluded_middle 1);
    7.77 -by( safe_tac (HOL_cs addSIs [subsetI]) );
    7.78 +by ( cut_inst_tac [("P","v:dom S")] excluded_middle 1);
    7.79 +by ( safe_tac (HOL_cs addSIs [subsetI]) );
    7.80  by (fast_tac (set_cs addss (!simpset addsimps [dom_def])) 1);
    7.81  by (fast_tac (set_cs addss (!simpset addsimps [cod_def])) 1);
    7.82  qed "free_tv_subst_var";
    7.83  
    7.84  goal thy 
    7.85       "free_tv ($ S (t::typ)) <= cod S Un free_tv t";
    7.86 -by( typ.induct_tac "t" 1);
    7.87 +by ( typ.induct_tac "t" 1);
    7.88  (* case TVar n *)
    7.89 -by( simp_tac (!simpset addsimps [free_tv_subst_var]) 1);
    7.90 +by ( simp_tac (!simpset addsimps [free_tv_subst_var]) 1);
    7.91  (* case Fun t1 t2 *)
    7.92 -by( fast_tac (set_cs addss !simpset) 1);
    7.93 +by ( fast_tac (set_cs addss !simpset) 1);
    7.94  qed "free_tv_app_subst_te";     
    7.95  
    7.96  goal thy 
    7.97       "free_tv ($ S (sch::type_scheme)) <= cod S Un free_tv sch";
    7.98 -by( type_scheme.induct_tac "sch" 1);
    7.99 +by ( type_scheme.induct_tac "sch" 1);
   7.100  (* case FVar n *)
   7.101 -by( simp_tac (!simpset addsimps [free_tv_subst_var]) 1);
   7.102 +by ( simp_tac (!simpset addsimps [free_tv_subst_var]) 1);
   7.103  (* case BVar n *)
   7.104  by (Simp_tac 1);
   7.105  (* case Fun t1 t2 *)
   7.106 @@ -306,12 +306,12 @@
   7.107  
   7.108  goal thy 
   7.109       "free_tv ($ S (A::type_scheme list)) <= cod S Un free_tv A";
   7.110 -by( list.induct_tac "A" 1);
   7.111 +by ( list.induct_tac "A" 1);
   7.112  (* case [] *)
   7.113  by (Simp_tac 1);
   7.114  (* case a#al *)
   7.115 -by( cut_facts_tac [free_tv_app_subst_type_scheme] 1);
   7.116 -by( fast_tac (set_cs addss !simpset) 1);
   7.117 +by ( cut_facts_tac [free_tv_app_subst_type_scheme] 1);
   7.118 +by ( fast_tac (set_cs addss !simpset) 1);
   7.119  qed "free_tv_app_subst_scheme_list";
   7.120  
   7.121  goalw thy [free_tv_subst,dom_def]
   7.122 @@ -396,29 +396,29 @@
   7.123  goalw thy [new_tv_def]
   7.124    "new_tv n S = ((!m. n <= m --> (S m = TVar m)) & \
   7.125  \                (! l. l < n --> new_tv n (S l) ))";
   7.126 -by( safe_tac HOL_cs );
   7.127 +by ( safe_tac HOL_cs );
   7.128  (* ==> *)
   7.129 -by( fast_tac (HOL_cs addDs [leD] addss (!simpset addsimps [free_tv_subst,dom_def])) 1);
   7.130 -by( subgoal_tac "m:cod S | S l = TVar l" 1);
   7.131 -by( safe_tac HOL_cs );
   7.132 -by(fast_tac (HOL_cs addDs [UnI2] addss (!simpset addsimps [free_tv_subst])) 1);
   7.133 -by(dres_inst_tac [("P","%x. m:free_tv x")] subst 1 THEN atac 1);
   7.134 -by(Asm_full_simp_tac 1);
   7.135 -by(fast_tac (set_cs addss (!simpset addsimps [free_tv_subst,cod_def,dom_def])) 1);
   7.136 +by ( fast_tac (HOL_cs addDs [leD] addss (!simpset addsimps [free_tv_subst,dom_def])) 1);
   7.137 +by ( subgoal_tac "m:cod S | S l = TVar l" 1);
   7.138 +by ( safe_tac HOL_cs );
   7.139 +by (fast_tac (HOL_cs addDs [UnI2] addss (!simpset addsimps [free_tv_subst])) 1);
   7.140 +by (dres_inst_tac [("P","%x. m:free_tv x")] subst 1 THEN atac 1);
   7.141 +by (Asm_full_simp_tac 1);
   7.142 +by (fast_tac (set_cs addss (!simpset addsimps [free_tv_subst,cod_def,dom_def])) 1);
   7.143  (* <== *)
   7.144 -by( rewrite_goals_tac [free_tv_subst,cod_def,dom_def] );
   7.145 -by( safe_tac set_cs );
   7.146 -by( cut_inst_tac [("m","m"),("n","n")] less_linear 1);
   7.147 -by( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
   7.148 -by( cut_inst_tac [("m","ma"),("n","n")] less_linear 1);
   7.149 -by( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
   7.150 +by ( rewrite_goals_tac [free_tv_subst,cod_def,dom_def] );
   7.151 +by ( safe_tac set_cs );
   7.152 +by ( cut_inst_tac [("m","m"),("n","n")] less_linear 1);
   7.153 +by ( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
   7.154 +by ( cut_inst_tac [("m","ma"),("n","n")] less_linear 1);
   7.155 +by ( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
   7.156  qed "new_tv_subst";
   7.157  
   7.158  goal thy 
   7.159    "new_tv n  = list_all (new_tv n)";
   7.160  by (rtac ext 1);
   7.161 -by(list.induct_tac "x" 1);
   7.162 -by(ALLGOALS Asm_simp_tac);
   7.163 +by (list.induct_tac "x" 1);
   7.164 +by (ALLGOALS Asm_simp_tac);
   7.165  qed "new_tv_list";
   7.166  
   7.167  (* substitution affects only variables occurring freely *)
   7.168 @@ -501,7 +501,7 @@
   7.169  
   7.170  goal thy
   7.171    "new_tv n A --> new_tv (Suc n) ((TVar n)#A)";
   7.172 -by( simp_tac (!simpset addsimps [new_tv_list]) 1);
   7.173 +by ( simp_tac (!simpset addsimps [new_tv_list]) 1);
   7.174  by (list.induct_tac "A" 1);
   7.175  by (ALLGOALS Asm_full_simp_tac);
   7.176  qed "new_tv_Suc_list";
   7.177 @@ -627,13 +627,13 @@
   7.178  by (cut_inst_tac [("t","t")] fresh_variable_types 1);
   7.179  by (cut_inst_tac [("t","t'")] fresh_variable_types 1);
   7.180  by (dtac make_one_new_out_of_two 1);
   7.181 -ba 1;
   7.182 +by (assume_tac 1);
   7.183  by (thin_tac "? n. new_tv n t'" 1);
   7.184  by (cut_inst_tac [("A","A")] fresh_variable_type_scheme_lists 1);
   7.185  by (cut_inst_tac [("A","A'")] fresh_variable_type_scheme_lists 1);
   7.186  by (rotate_tac 1 1);
   7.187  by (dtac make_one_new_out_of_two 1);
   7.188 -ba 1;
   7.189 +by (assume_tac 1);
   7.190  by (thin_tac "? n. new_tv n A'" 1);
   7.191  by (REPEAT (etac exE 1));
   7.192  by (rename_tac "n2 n1" 1);
   7.193 @@ -646,14 +646,14 @@
   7.194  goalw thy [new_tv_def] 
   7.195        "!! n. [|mgu t1 t2 = Some u; new_tv n t1; new_tv n t2|] ==> \
   7.196  \            new_tv n u";
   7.197 -by( fast_tac (set_cs addDs [mgu_free]) 1);
   7.198 +by ( fast_tac (set_cs addDs [mgu_free]) 1);
   7.199  qed "mgu_new";
   7.200  
   7.201  
   7.202  (* lemmata for substitutions *)
   7.203  
   7.204  goalw Type.thy [app_subst_list] "length ($ S A) = length A";
   7.205 -by(Simp_tac 1);
   7.206 +by (Simp_tac 1);
   7.207  qed "length_app_subst_list";
   7.208  Addsimps [length_app_subst_list];
   7.209  
   7.210 @@ -714,8 +714,8 @@
   7.211  
   7.212  (* composition of substitutions *)
   7.213  goalw Type.thy [id_subst_def,o_def] "$S o id_subst = S";
   7.214 -br ext 1;
   7.215 -by(Simp_tac 1);
   7.216 +by (rtac ext 1);
   7.217 +by (Simp_tac 1);
   7.218  qed "o_id_subst";
   7.219  Addsimps[o_id_subst];
   7.220  
   7.221 @@ -747,7 +747,7 @@
   7.222  
   7.223  goal thy "!!A::type_scheme list. !x : free_tv A. S x = (TVar x) ==> $ S A = A";
   7.224  by (stac subst_id_on_type_scheme_list' 1);
   7.225 -ba 1;
   7.226 +by (assume_tac 1);
   7.227  by (Simp_tac 1);
   7.228  qed "subst_id_on_type_scheme_list";
   7.229  
     8.1 --- a/src/HOL/MiniML/W.ML	Wed Apr 23 11:00:48 1997 +0200
     8.2 +++ b/src/HOL/MiniML/W.ML	Wed Apr 23 11:02:19 1997 +0200
     8.3 @@ -70,8 +70,8 @@
     8.4  goal thy "!! s. new_tv n A ==> Some (S,t,m) = W e A n ==> new_tv m A";
     8.5  by (dtac W_var_geD 1);
     8.6  by (rtac new_scheme_list_le 1);
     8.7 -ba 1;
     8.8 -ba 1;
     8.9 +by (assume_tac 1);
    8.10 +by (assume_tac 1);
    8.11  qed "new_tv_compatible_W";
    8.12  
    8.13  goal thy "!!sch. new_tv n sch --> new_tv (n + (min_new_bound_tv sch)) (bound_typ_inst (%b. TVar (b + n)) sch)";
    8.14 @@ -85,7 +85,7 @@
    8.15  by (rtac new_tv_le 1);
    8.16  by (mp_tac 2);
    8.17  by (mp_tac 2);
    8.18 -ba 2;
    8.19 +by (assume_tac 2);
    8.20  by (rtac add_le_mono 1);
    8.21  by (Simp_tac 1);
    8.22  by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [max_def]) 1);
    8.23 @@ -93,7 +93,7 @@
    8.24  by (rtac new_tv_le 1);
    8.25  by (mp_tac 2);
    8.26  by (mp_tac 2);
    8.27 -ba 2;
    8.28 +by (assume_tac 2);
    8.29  by (rtac add_le_mono 1);
    8.30  by (Simp_tac 1);
    8.31  by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [max_def]) 1);
    8.32 @@ -121,7 +121,7 @@
    8.33  by (dtac sym 1);
    8.34  by (dtac sym 1);
    8.35  by (dtac new_tv_nth_nat_A 1);
    8.36 -ba 1;
    8.37 +by (assume_tac 1);
    8.38  by (Asm_full_simp_tac 1);
    8.39  (* case Abs e *)
    8.40  by (simp_tac (!simpset addsimps [new_tv_subst,new_tv_Suc_list] 
    8.41 @@ -146,7 +146,7 @@
    8.42  by (eres_inst_tac [("x","S1")] allE 1);
    8.43  by (eres_inst_tac [("x","t1")] allE 1);
    8.44  by (eres_inst_tac [("x","n2")] allE 1);
    8.45 -by( asm_full_simp_tac (!simpset addsimps [o_def,rotate_Some]) 1);
    8.46 +by ( asm_full_simp_tac (!simpset addsimps [o_def,rotate_Some]) 1);
    8.47  by (rtac conjI 1);
    8.48  by (rtac new_tv_subst_comp_2 1);
    8.49  by (rtac new_tv_subst_comp_2 1);
    8.50 @@ -203,9 +203,9 @@
    8.51  by (rtac new_tv_subst_comp_2 1);
    8.52  by (res_inst_tac [("n","n2")] new_tv_subst_le 1);
    8.53  by (etac W_var_ge 1);
    8.54 -ba 1;
    8.55 -ba 1;
    8.56 -ba 1;
    8.57 +by (assume_tac 1);
    8.58 +by (assume_tac 1);
    8.59 +by (assume_tac 1);
    8.60  by (rewtac new_tv_def);
    8.61  by (Asm_simp_tac 1);
    8.62  by (dtac W_var_ge 1);
    8.63 @@ -356,12 +356,12 @@
    8.64  by (Asm_full_simp_tac 1);
    8.65  by (rtac has_type.AbsI 1);
    8.66  by (dtac (le_refl RS le_SucI RS new_scheme_list_le) 1);
    8.67 -bd sym 1;
    8.68 +by (dtac sym 1);
    8.69  by (REPEAT (etac allE 1));
    8.70  by (etac impE 1);
    8.71  by (mp_tac 2);
    8.72  by (Asm_simp_tac 1);
    8.73 -ba 1;
    8.74 +by (assume_tac 1);
    8.75  (* case App e1 e2 *)
    8.76  by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
    8.77  by (strip_tac 1);
    8.78 @@ -377,23 +377,23 @@
    8.79  by (asm_full_simp_tac (!simpset addsimps [subst_comp_scheme_list RS sym,o_def,has_type_cl_sub,eq_sym_conv]) 1);
    8.80  by (rtac (has_type_cl_sub RS spec) 1);
    8.81  by (forward_tac [new_tv_W] 1);
    8.82 -ba 1;
    8.83 +by (assume_tac 1);
    8.84  by (dtac conjunct1 1);
    8.85  by (dtac conjunct1 1);
    8.86  by (forward_tac [new_tv_subst_scheme_list] 1);
    8.87  by (rtac new_scheme_list_le 1);
    8.88  by (rtac W_var_ge 1);
    8.89 -ba 1;
    8.90 -ba 1;
    8.91 +by (assume_tac 1);
    8.92 +by (assume_tac 1);
    8.93  by (etac thin_rl 1);
    8.94  by (REPEAT (etac allE 1));
    8.95 -bd sym 1;
    8.96 -bd sym 1;
    8.97 +by (dtac sym 1);
    8.98 +by (dtac sym 1);
    8.99  by (etac thin_rl 1);
   8.100  by (etac thin_rl 1);
   8.101  by (mp_tac 1);
   8.102  by (mp_tac 1);
   8.103 -ba 1;
   8.104 +by (assume_tac 1);
   8.105  (* case Let e1 e2 *)
   8.106  by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
   8.107  by (strip_tac 1);
   8.108 @@ -421,19 +421,19 @@
   8.109  by (dres_inst_tac [("x","n2")] spec 2);
   8.110  by (dres_inst_tac [("x","m2")] spec 2);
   8.111  by (forward_tac [new_tv_W] 2);
   8.112 -ba 2;
   8.113 +by (assume_tac 2);
   8.114  by (dtac conjunct1 2);
   8.115  by (dtac conjunct1 2);
   8.116  by (forward_tac [new_tv_subst_scheme_list] 2);
   8.117  by (rtac new_scheme_list_le 2);
   8.118  by (rtac W_var_ge 2);
   8.119 -ba 2;
   8.120 -ba 2;
   8.121 +by (assume_tac 2);
   8.122 +by (assume_tac 2);
   8.123  by (etac impE 2);
   8.124  by (res_inst_tac [("A","$ S1 A")] new_tv_only_depends_on_free_tv_scheme_list 2);
   8.125  by (Simp_tac 2);
   8.126  by (Fast_tac 2);
   8.127 -ba 2;
   8.128 +by (assume_tac 2);
   8.129  by (Asm_full_simp_tac 2);
   8.130  by (rtac weaken_A_Int_B_eq_empty 1);
   8.131  by (rtac allI 1);
   8.132 @@ -443,24 +443,24 @@
   8.133  by (rtac disjI2 1);
   8.134  by (rtac (free_tv_gen_cons RS subst) 1);
   8.135  by (rtac free_tv_W 1);
   8.136 -ba 1;
   8.137 +by (assume_tac 1);
   8.138  by (Asm_full_simp_tac 1);
   8.139 -ba 1;
   8.140 +by (assume_tac 1);
   8.141  by (rtac disjI1 1);
   8.142  by (dtac new_tv_W 1);
   8.143 -ba 1;
   8.144 +by (assume_tac 1);
   8.145  by (dtac conjunct2 1);
   8.146  by (dtac conjunct2 1);
   8.147  by (rtac new_tv_not_free_tv 1);
   8.148  by (rtac new_tv_le 1);
   8.149 -ba 2;
   8.150 +by (assume_tac 2);
   8.151  by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le]) 1);
   8.152  qed_spec_mp "W_correct_lemma";
   8.153  
   8.154  goal Arith.thy "!!n::nat. ~ k+n < n";
   8.155  by (nat_ind_tac "k" 1);
   8.156 -by(ALLGOALS Asm_simp_tac);
   8.157 -by(trans_tac 1);
   8.158 +by (ALLGOALS Asm_simp_tac);
   8.159 +by (trans_tac 1);
   8.160  val not_add_less1 = result();
   8.161  Addsimps [not_add_less1];
   8.162  
   8.163 @@ -567,10 +567,10 @@
   8.164  by (fast_tac (HOL_cs addDs [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_W,new_tv_not_free_tv]) 3);
   8.165  by (case_tac "na: free_tv t - free_tv Sa" 2);
   8.166  (* case na ~: free_tv t - free_tv Sa *)
   8.167 -by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
   8.168 +by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
   8.169  by (Fast_tac 3);
   8.170  (* case na : free_tv t - free_tv Sa *)
   8.171 -by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
   8.172 +by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
   8.173  by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
   8.174  by (dtac eq_subst_scheme_list_eq_free 2);
   8.175  by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
   8.176 @@ -579,21 +579,21 @@
   8.177  by (asm_simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1); 
   8.178  by (safe_tac HOL_cs );
   8.179  by (dtac mgu_Some 1);
   8.180 -by( fast_tac (HOL_cs addss !simpset) 1);
   8.181 +by ( fast_tac (HOL_cs addss !simpset) 1);
   8.182  (** LEVEL 80 *)
   8.183  by ((dtac mgu_mg 1) THEN (atac 1));
   8.184  by (etac exE 1);
   8.185  by (res_inst_tac [("x","Rb")] exI 1);
   8.186  by (rtac conjI 1);
   8.187  by (dres_inst_tac [("x","ma")] fun_cong 2);
   8.188 -by( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2);
   8.189 +by ( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2);
   8.190  by (simp_tac (!simpset addsimps [subst_comp_scheme_list]) 1);
   8.191  by (simp_tac (!simpset addsimps [subst_comp_scheme_list RS sym]) 1);
   8.192  by (res_inst_tac [("A2","($ Sa ($ S A))")]
   8.193         ((subst_comp_scheme_list RS sym) RSN (2,trans)) 1);
   8.194 -by( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1);
   8.195 +by ( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1);
   8.196  by (rtac eq_free_eq_subst_scheme_list 1);
   8.197 -by( safe_tac HOL_cs );
   8.198 +by ( safe_tac HOL_cs );
   8.199  by (subgoal_tac "ma ~= na" 1);
   8.200  by ((forward_tac [new_tv_W] 2) THEN (atac 2));
   8.201  by (etac conjE 2);
   8.202 @@ -632,13 +632,13 @@
   8.203  by (Asm_full_simp_tac 1);
   8.204  by (dtac mp 1);
   8.205  by (rtac has_type_le_env 1);
   8.206 -ba 1;
   8.207 +by (assume_tac 1);
   8.208  by (Simp_tac 1);
   8.209  by (rtac gen_bound_typ_instance 1);
   8.210  by (dtac mp 1);
   8.211  by (forward_tac [new_tv_compatible_W] 1);
   8.212  by (rtac sym 1);
   8.213 -ba 1;
   8.214 +by (assume_tac 1);
   8.215  by (fast_tac (!claset addDs [new_tv_compatible_gen,new_tv_subst_scheme_list,new_tv_W]) 1);
   8.216  by (safe_tac HOL_cs);
   8.217  by (Asm_full_simp_tac 1);
   8.218 @@ -649,7 +649,7 @@
   8.219  goal W.thy
   8.220   "!!e. [] |- e :: t' ==>  (? S t. (? m. W e [] n = Some(S,t,m)) &  \
   8.221  \                                 (? R. t' = $ R t))";
   8.222 -by(cut_inst_tac [("A","[]"),("S'","id_subst"),("e","e"),("t'","t'")]
   8.223 +by (cut_inst_tac [("A","[]"),("S'","id_subst"),("e","e"),("t'","t'")]
   8.224                  W_complete_lemma 1);
   8.225 -by(ALLGOALS Asm_full_simp_tac);
   8.226 +by (ALLGOALS Asm_full_simp_tac);
   8.227  qed "W_complete";
     9.1 --- a/src/HOL/W0/W.ML	Wed Apr 23 11:00:48 1997 +0200
     9.2 +++ b/src/HOL/W0/W.ML	Wed Apr 23 11:02:19 1997 +0200
     9.3 @@ -19,7 +19,7 @@
     9.4  by (asm_full_simp_tac (!simpset addsimps [app_subst_list]
     9.5                          setloop (split_tac [expand_bind])) 1);
     9.6  by (strip_tac 1);
     9.7 -bd sym 1;
     9.8 +by (dtac sym 1);
     9.9  by (fast_tac (HOL_cs addss !simpset) 1);
    9.10  (* case App e1 e2 *)
    9.11  by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
    10.1 --- a/src/HOL/ex/LFilter.ML	Wed Apr 23 11:00:48 1997 +0200
    10.2 +++ b/src/HOL/ex/LFilter.ML	Wed Apr 23 11:02:19 1997 +0200
    10.3 @@ -19,13 +19,13 @@
    10.4  
    10.5  
    10.6  goal thy "!!p. (l,l'): findRel p ==> (l,l''): findRel p --> l'' = l'";
    10.7 -be findRel.induct 1;
    10.8 +by (etac findRel.induct 1);
    10.9  by (Blast_tac 1);
   10.10  by (Blast_tac 1);
   10.11  qed_spec_mp "findRel_functional";
   10.12  
   10.13  goal thy "!!p. (l,l'): findRel p ==> EX x l''. l' = LCons x l'' & p x";
   10.14 -be findRel.induct 1;
   10.15 +by (etac findRel.induct 1);
   10.16  by (Blast_tac 1);
   10.17  by (Blast_tac 1);
   10.18  qed_spec_mp "findRel_imp_LCons";
   10.19 @@ -50,7 +50,7 @@
   10.20  goal thy "[| l: Domain (findRel p);                                   \
   10.21  \            !!x l'. [| (l, LCons x l') : findRel p;  p x |] ==> Q    \
   10.22  \         |] ==> Q";
   10.23 -br (major RS DomainE) 1;
   10.24 +by (rtac (major RS DomainE) 1);
   10.25  by (forward_tac [findRel_imp_LCons] 1);
   10.26  by (REPEAT (eresolve_tac [exE,conjE] 1));
   10.27  by (hyp_subst_tac 1);
   10.28 @@ -60,7 +60,7 @@
   10.29  val prems = goal thy
   10.30      "[| !!x. p x ==> q x |] ==> Domain (findRel p) <= Domain (findRel q)";
   10.31  by (Step_tac 1);
   10.32 -be findRel.induct 1;
   10.33 +by (etac findRel.induct 1);
   10.34  by (blast_tac (!claset addIs (findRel.intrs@prems)) 1);
   10.35  by (blast_tac (!claset addIs findRel.intrs) 1);
   10.36  qed "Domain_findRel_mono";
   10.37 @@ -96,7 +96,7 @@
   10.38  
   10.39  goal thy "find p (LCons x l) = (if p x then LCons x l else find p l)";
   10.40  by (asm_simp_tac (!simpset addsimps [find_LCons_found, find_LCons_seek]
   10.41 -		           setloop split_tac[expand_if]) 1);
   10.42 +                           setloop split_tac[expand_if]) 1);
   10.43  qed "find_LCons";
   10.44  
   10.45  
   10.46 @@ -130,18 +130,18 @@
   10.47  by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
   10.48  by (case_tac "LCons x l : Domain(findRel p)" 1);
   10.49  by (asm_full_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
   10.50 -be Domain_findRelE 1;
   10.51 +by (etac Domain_findRelE 1);
   10.52  by (safe_tac (!claset delrules [conjI]));
   10.53  by (asm_full_simp_tac 
   10.54      (!simpset addsimps [findRel_imp_lfilter, findRel_imp_find,
   10.55 -			find_LCons_seek]) 1);
   10.56 +                        find_LCons_seek]) 1);
   10.57  qed "lfilter_LCons_seek";
   10.58  
   10.59  
   10.60  goal thy "lfilter p (LCons x l) = \
   10.61  \         (if p x then LCons x (lfilter p l) else lfilter p l)";
   10.62  by (asm_simp_tac (!simpset addsimps [lfilter_LCons_found, lfilter_LCons_seek]
   10.63 -		           setloop split_tac[expand_if]) 1);
   10.64 +                           setloop split_tac[expand_if]) 1);
   10.65  qed "lfilter_LCons";
   10.66  
   10.67  AddSIs [llistD_Fun_LNil_I, llistD_Fun_LCons_I];
   10.68 @@ -149,9 +149,9 @@
   10.69  
   10.70  
   10.71  goal thy "!!p. lfilter p l = LNil ==> l ~: Domain(findRel p)";
   10.72 -br notI 1;
   10.73 -be Domain_findRelE 1;
   10.74 -be rev_mp 1;
   10.75 +by (rtac notI 1);
   10.76 +by (etac Domain_findRelE 1);
   10.77 +by (etac rev_mp 1);
   10.78  by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
   10.79  qed "lfilter_eq_LNil";
   10.80  
   10.81 @@ -160,7 +160,7 @@
   10.82  \              (EX l''. l' = lfilter p l'' & (l, LCons x l'') : findRel p)";
   10.83  by (stac (lfilter_def RS def_llist_corec) 1);
   10.84  by (case_tac "l : Domain(findRel p)" 1);
   10.85 -be Domain_findRelE 1;
   10.86 +by (etac Domain_findRelE 1);
   10.87  by (Asm_simp_tac 2);
   10.88  by (asm_simp_tac (!simpset addsimps [findRel_imp_find]) 1);
   10.89  by (Blast_tac 1);
   10.90 @@ -190,8 +190,8 @@
   10.91  by (Step_tac 1);
   10.92  (*Cases: p x is true or false*)
   10.93  by (Blast_tac 1);
   10.94 -br (lfilter_cases RS disjE) 1;
   10.95 -be ssubst 1;
   10.96 +by (rtac (lfilter_cases RS disjE) 1);
   10.97 +by (etac ssubst 1);
   10.98  by (Auto_tac());
   10.99  qed "lfilter_idem";
  10.100  
  10.101 @@ -202,7 +202,7 @@
  10.102  
  10.103  goal thy "!!p. (l,l') : findRel q \
  10.104  \           ==> l' = LCons x l'' --> p x --> (l,l') : findRel (%x. p x & q x)";
  10.105 -be findRel.induct 1;
  10.106 +by (etac findRel.induct 1);
  10.107  by (blast_tac (!claset addIs findRel.intrs) 1);
  10.108  by (blast_tac (!claset addIs findRel.intrs) 1);
  10.109  qed_spec_mp "findRel_conj_lemma";
  10.110 @@ -212,7 +212,7 @@
  10.111  goal thy "!!p. (l,l'') : findRel (%x. p x & q x) \
  10.112  \              ==> (l, LCons x l') : findRel q --> ~ p x     \
  10.113  \                  --> l' : Domain (findRel (%x. p x & q x))";
  10.114 -be findRel.induct 1;
  10.115 +by (etac findRel.induct 1);
  10.116  by (Auto_tac());
  10.117  qed_spec_mp "findRel_not_conj_Domain";
  10.118  
  10.119 @@ -220,7 +220,7 @@
  10.120  goal thy "!!p. (l,lxx) : findRel q ==> \
  10.121  \            lxx = LCons x lx --> (lx,lz) : findRel(%x. p x & q x) --> ~ p x \
  10.122  \            --> (l,lz) : findRel (%x. p x & q x)";
  10.123 -be findRel.induct 1;
  10.124 +by (etac findRel.induct 1);
  10.125  by (ALLGOALS (blast_tac (!claset addIs findRel.intrs)));
  10.126  qed_spec_mp "findRel_conj2";
  10.127  
  10.128 @@ -228,14 +228,14 @@
  10.129  goal thy "!!p. (lx,ly) : findRel p \
  10.130  \              ==> ALL l. lx = lfilter q l \
  10.131  \                  --> l : Domain (findRel(%x. p x & q x))";
  10.132 -be findRel.induct 1;
  10.133 +by (etac findRel.induct 1);
  10.134  by (blast_tac (!claset addSDs [sym RS lfilter_eq_LCons]
  10.135 -	               addIs  [findRel_conj]) 1);
  10.136 +                       addIs  [findRel_conj]) 1);
  10.137  by (Auto_tac());
  10.138 -bd (sym RS lfilter_eq_LCons) 1;
  10.139 +by (dtac (sym RS lfilter_eq_LCons) 1);
  10.140  by (Auto_tac());
  10.141 -bd spec 1;
  10.142 -bd (refl RS rev_mp) 1;
  10.143 +by (dtac spec 1);
  10.144 +by (dtac (refl RS rev_mp) 1);
  10.145  by (blast_tac (!claset addIs [findRel_conj2]) 1);
  10.146  qed_spec_mp "findRel_lfilter_Domain_conj";
  10.147  
  10.148 @@ -243,7 +243,7 @@
  10.149  goal thy "!!p. (l,l'') : findRel(%x. p x & q x) \
  10.150  \              ==> l'' = LCons y l' --> \
  10.151  \                  (lfilter q l, LCons y (lfilter q l')) : findRel p";
  10.152 -be findRel.induct 1;
  10.153 +by (etac findRel.induct 1);
  10.154  by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac[expand_if])));
  10.155  by (ALLGOALS (blast_tac (!claset addIs findRel.intrs)));
  10.156  qed_spec_mp "findRel_conj_lfilter";
  10.157 @@ -263,7 +263,7 @@
  10.158  (*case q x*)
  10.159  by (case_tac "p x" 1);
  10.160  by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter,
  10.161 -				     findRel_conj RS findRel_imp_lfilter]) 1);
  10.162 +                                     findRel_conj RS findRel_imp_lfilter]) 1);
  10.163  by (Blast_tac 1);
  10.164  (*case q x and ~(p x) *)
  10.165  by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
  10.166 @@ -276,7 +276,7 @@
  10.167  (*    ...and therefore too, no p in lfilter q l'.  Both results are Lnil*)
  10.168  by (asm_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
  10.169  (*subcase: there is a p&q in l' and therefore also one in l*)
  10.170 -be Domain_findRelE 1;
  10.171 +by (etac Domain_findRelE 1);
  10.172  by (subgoal_tac "(l, LCons xa l'a) : findRel(%x. p x & q x)" 1);
  10.173  by (blast_tac (!claset addIs [findRel_conj2]) 2);
  10.174  by (subgoal_tac "(lfilter q l', LCons xa (lfilter q l'a)) : findRel p" 1);
  10.175 @@ -298,7 +298,7 @@
  10.176   ***)
  10.177  
  10.178  goal thy "!!p. (l,l') : findRel(%x. p (f x)) ==> lmap f l : Domain(findRel p)";
  10.179 -be findRel.induct 1;
  10.180 +by (etac findRel.induct 1);
  10.181  by (ALLGOALS Asm_full_simp_tac);
  10.182  qed "findRel_lmap_Domain";
  10.183  
  10.184 @@ -315,7 +315,7 @@
  10.185  \    ALL l. lmap f l = lx --> ly = LCons x l' --> \
  10.186  \    (EX y l''. x = f y & l' = lmap f l'' &       \
  10.187  \    (l, LCons y l'') : findRel(%x. p(f x)))";
  10.188 -be findRel.induct 1;
  10.189 +by (etac findRel.induct 1);
  10.190  by (ALLGOALS Asm_simp_tac);
  10.191  by (safe_tac (!claset addSDs [lmap_eq_LCons]));
  10.192  by (blast_tac (!claset addIs findRel.intrs) 1);
  10.193 @@ -333,7 +333,7 @@
  10.194  by (subgoal_tac "l ~: Domain (findRel(%x. p (f x)))" 2);
  10.195  by (blast_tac (!claset addIs [findRel_lmap_Domain]) 3);
  10.196  by (asm_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
  10.197 -be Domain_findRelE 1;
  10.198 +by (etac Domain_findRelE 1);
  10.199  by (forward_tac [lmap_LCons_findRel] 1);
  10.200  by (Step_tac 1);
  10.201  by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
    11.1 --- a/src/HOL/ex/LList.ML	Wed Apr 23 11:00:48 1997 +0200
    11.2 +++ b/src/HOL/ex/LList.ML	Wed Apr 23 11:02:19 1997 +0200
    11.3 @@ -649,7 +649,7 @@
    11.4  goalw thy [llistD_Fun_def, prod_fun_def]
    11.5      "!!A B. A<=B ==> llistD_Fun A <= llistD_Fun B";
    11.6  by (Auto_tac());
    11.7 -br image_eqI 1;
    11.8 +by (rtac image_eqI 1);
    11.9  by (fast_tac (!claset addss (!simpset)) 1);
   11.10  by (blast_tac (!claset addIs [impOfSubs LListD_Fun_mono]) 1);
   11.11  qed "llistD_Fun_mono";
    12.1 --- a/src/HOLCF/Discrete0.ML	Wed Apr 23 11:00:48 1997 +0200
    12.2 +++ b/src/HOLCF/Discrete0.ML	Wed Apr 23 11:02:19 1997 +0200
    12.3 @@ -7,16 +7,16 @@
    12.4  *)
    12.5  
    12.6  goalw thy [less_discr_def] "less (x::('a::term)discr) x";
    12.7 -br refl 1;
    12.8 +by (rtac refl 1);
    12.9  qed "less_discr_refl";
   12.10  
   12.11  goalw thy [less_discr_def]
   12.12    "!!x. [| less (x::('a::term)discr) y; less y z |] ==> less x z";
   12.13 -be trans 1;
   12.14 -ba 1;
   12.15 +by (etac trans 1);
   12.16 +by (assume_tac 1);
   12.17  qed "less_discr_trans";
   12.18  
   12.19  goalw thy [less_discr_def]
   12.20    "!!x. [| less (x::('a::term)discr) y; less y x |] ==> x=y";
   12.21 -ba 1;
   12.22 +by (assume_tac 1);
   12.23  qed "less_discr_antisym";
    13.1 --- a/src/HOLCF/Discrete1.ML	Wed Apr 23 11:00:48 1997 +0200
    13.2 +++ b/src/HOLCF/Discrete1.ML	Wed Apr 23 11:02:19 1997 +0200
    13.3 @@ -7,26 +7,26 @@
    13.4  *)
    13.5  
    13.6  goalw thy [po_def,less_discr_def] "((x::('a::term)discr) << y) = (x=y)";
    13.7 -br refl 1;
    13.8 +by (rtac refl 1);
    13.9  qed "discr_less_eq";
   13.10  AddIffs [discr_less_eq];
   13.11  
   13.12  goalw thy [is_chain]
   13.13   "!!S::nat=>('a::term)discr. is_chain S ==> S i = S 0";
   13.14 -by(nat_ind_tac "i" 1);
   13.15 - br refl 1;
   13.16 -be subst 1;
   13.17 -br sym 1;
   13.18 -by(Fast_tac 1);
   13.19 +by (nat_ind_tac "i" 1);
   13.20 + by (rtac refl 1);
   13.21 +by (etac subst 1);
   13.22 +by (rtac sym 1);
   13.23 +by (Fast_tac 1);
   13.24  qed "discr_chain0";
   13.25  
   13.26  goal thy
   13.27   "!!S::nat=>('a::term)discr. is_chain(S) ==> range(S) = {S 0}";
   13.28 -by(fast_tac (!claset addEs [discr_chain0]) 1);
   13.29 +by (fast_tac (!claset addEs [discr_chain0]) 1);
   13.30  qed "discr_chain_range0";
   13.31  Addsimps [discr_chain_range0];
   13.32  
   13.33  goalw thy [is_lub,is_ub]
   13.34   "!!S. is_chain S ==> ? x::('a::term)discr. range(S) <<| x";
   13.35 -by(Asm_simp_tac 1);
   13.36 +by (Asm_simp_tac 1);
   13.37  qed "discr_cpo";
    14.1 --- a/src/HOLCF/Porder.ML	Wed Apr 23 11:00:48 1997 +0200
    14.2 +++ b/src/HOLCF/Porder.ML	Wed Apr 23 11:02:19 1997 +0200
    14.3 @@ -137,8 +137,8 @@
    14.4  
    14.5  
    14.6  goal thy "lub{x} = x";
    14.7 -br thelubI 1;
    14.8 -by(simp_tac (!simpset addsimps [is_lub,is_ub]) 1);
    14.9 +by (rtac thelubI 1);
   14.10 +by (simp_tac (!simpset addsimps [is_lub,is_ub]) 1);
   14.11  qed "lub_singleton";
   14.12  Addsimps [lub_singleton];
   14.13  
    15.1 --- a/src/HOLCF/ex/Focus_ex.ML	Wed Apr 23 11:00:48 1997 +0200
    15.2 +++ b/src/HOLCF/ex/Focus_ex.ML	Wed Apr 23 11:02:19 1997 +0200
    15.3 @@ -75,7 +75,7 @@
    15.4  by (strip_tac 1);
    15.5  by (rtac fix_least 1);
    15.6  by (Simp_tac 1);
    15.7 -by(etac exE 1);
    15.8 +by (etac exE 1);
    15.9  by (dtac sym 1);
   15.10  back();
   15.11  by (asm_simp_tac HOLCF_ss 1);
   15.12 @@ -84,7 +84,7 @@
   15.13  (* direction is_g(g) --> def_g(g) *)
   15.14  val prems = goal Focus_ex.thy "is_g(g) --> def_g(g)";
   15.15  by (simp_tac (HOL_ss delsimps (ex_simps @ all_simps)
   15.16 -		     addsimps [lemma1,lemma2,def_g]) 1);
   15.17 +                     addsimps [lemma1,lemma2,def_g]) 1);
   15.18  by (rtac impI 1);
   15.19  by (etac exE 1);
   15.20  by (res_inst_tac [("x","f")] exI 1);