# HG changeset patch
# User paulson
# Date 861786139 -7200
# Node ID e65b60b28341bc0580c46c648c69c5cf22a16121
# Parent  84c2178db936a6330498885d19b24de875e4b9d8
Ran expandshort

diff -r 84c2178db936 -r e65b60b28341 src/HOL/Integ/Group.ML
--- a/src/HOL/Integ/Group.ML	Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOL/Integ/Group.ML	Wed Apr 23 11:02:19 1997 +0200
@@ -9,78 +9,78 @@
 Addsimps [zeroL,zeroR,plus_assoc,plus_commute];
 
 goal Group.thy "!!x::'a::add_group. (zero-x)+(x+y) = y";
-br trans 1;
-br (plus_assoc RS sym) 1;
-by(stac left_inv 1);
-br zeroL 1;
+by (rtac trans 1);
+by (rtac (plus_assoc RS sym) 1);
+by (stac left_inv 1);
+by (rtac zeroL 1);
 qed "left_inv2";
 
 goal Group.thy "!!x::'a::add_group. (zero-(zero-x)) = x";
-br trans 1;
-by(res_inst_tac [("x","zero-x")] left_inv2 2);
-by(stac left_inv 1);
-br (zeroR RS sym) 1;
+by (rtac trans 1);
+by (res_inst_tac [("x","zero-x")] left_inv2 2);
+by (stac left_inv 1);
+by (rtac (zeroR RS sym) 1);
 qed "inv_inv";
 
 goal Group.thy "zero-zero = (zero::'a::add_group)";
-br trans 1;
-br (zeroR RS sym) 1;
-br trans 1;
-by(res_inst_tac [("x","zero")] left_inv2 2);
-by(Simp_tac 1);
+by (rtac trans 1);
+by (rtac (zeroR RS sym) 1);
+by (rtac trans 1);
+by (res_inst_tac [("x","zero")] left_inv2 2);
+by (Simp_tac 1);
 qed "inv_zero";
 
 goal Group.thy "!!x::'a::add_group. x+(zero-x) = zero";
-br trans 1;
-by(res_inst_tac [("x","zero-x")] left_inv 2);
-by(stac inv_inv 1);
-br refl 1;
+by (rtac trans 1);
+by (res_inst_tac [("x","zero-x")] left_inv 2);
+by (stac inv_inv 1);
+by (rtac refl 1);
 qed "right_inv";
 
 goal Group.thy "!!x::'a::add_group. x+((zero-x)+y) = y";
-br trans 1;
-by(res_inst_tac [("x","zero-x")] left_inv2 2);
-by(stac inv_inv 1);
-br refl 1;
+by (rtac trans 1);
+by (res_inst_tac [("x","zero-x")] left_inv2 2);
+by (stac inv_inv 1);
+by (rtac refl 1);
 qed "right_inv2";
 
 goal Group.thy "!!x::'a::add_group. x-x = zero";
-by(stac minus_inv 1);
-br right_inv 1;
+by (stac minus_inv 1);
+by (rtac right_inv 1);
 qed "minus_self_zero";
 Addsimps [minus_self_zero];
 
 goal Group.thy "!!x::'a::add_group. x-zero = x";
-by(stac minus_inv 1);
-by(stac inv_zero 1);
-br zeroR 1;
+by (stac minus_inv 1);
+by (stac inv_zero 1);
+by (rtac zeroR 1);
 qed "minus_zero";
 Addsimps [minus_zero];
 
 val plus_cong = read_instantiate [("f1","op +")] (arg_cong RS cong);
 
 goal Group.thy "!!x::'a::add_group. zero-(x+y) = (zero-y)+(zero-x)";
-br trans 1;
- br zeroR 2;
-br trans 1;
- br plus_cong 2;
-  br refl 2;
- by(res_inst_tac [("x","x+y")] right_inv 2);
-br trans 1;
- br plus_assoc 2;
-br trans 1;
- br plus_cong 2;
-  by(simp_tac (!simpset addsimps [left_inv,left_inv2,right_inv,right_inv2]) 2);
- br refl 2;
-br (zeroL RS sym) 1;
+by (rtac trans 1);
+ by (rtac zeroR 2);
+by (rtac trans 1);
+ by (rtac plus_cong 2);
+  by (rtac refl 2);
+ by (res_inst_tac [("x","x+y")] right_inv 2);
+by (rtac trans 1);
+ by (rtac plus_assoc 2);
+by (rtac trans 1);
+ by (rtac plus_cong 2);
+  by (simp_tac (!simpset addsimps [left_inv,left_inv2,right_inv,right_inv2]) 2);
+ by (rtac refl 2);
+by (rtac (zeroL RS sym) 1);
 qed "inv_plus";
 
 goal Group.thy "x+(y+z)=y+(x+z::'a::add_agroup)";
-br trans 1;
-br plus_commute 1;
-br trans 1;
-br plus_assoc 1;
-by(Simp_tac 1);
+by (rtac trans 1);
+by (rtac plus_commute 1);
+by (rtac trans 1);
+by (rtac plus_assoc 1);
+by (Simp_tac 1);
 qed "plus_commuteL";
 Addsimps [plus_commuteL];
 
@@ -89,39 +89,39 @@
 (* Phase 1 *)
 
 goal Group.thy "!!x::'a::add_agroup. (x+(zero-y))+z = (x+z)+(zero-y)";
-by(Simp_tac 1);
+by (Simp_tac 1);
 val lemma = result();
 bind_thm("plus_minusL",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
 
 goal Group.thy "!!x::'a::add_agroup. x+(zero-(y+z)) = (x+(zero-y))+(zero-z)";
-by(Simp_tac 1);
+by (Simp_tac 1);
 val lemma = result();
 bind_thm("minus_plusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
 
 goal Group.thy "!!x::'a::add_agroup. x+(zero-(y+(zero-z))) = (x+z)+(zero-y)";
-by(Simp_tac 1);
+by (Simp_tac 1);
 val lemma = result();
 bind_thm("minus_minusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
 
 goal Group.thy "!!x::'a::add_agroup. x+(y+(zero-z)) = (x+y)+(zero-z)";
-by(Simp_tac 1);
+by (Simp_tac 1);
 val lemma = result();
 bind_thm("plus_minusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
 
 (* Phase 2 *)
 
 goal Group.thy "!!x::'a::add_agroup. (x+y)+(zero-z) = x+(y+(zero-z))";
-by(Simp_tac 1);
+by (Simp_tac 1);
 val lemma = result();
 bind_thm("minus_plusL2",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
 
 goal Group.thy "!!x::'a::add_agroup. (x+y)+(zero-x) = y";
-br (plus_assoc RS trans) 1;
-br trans 1;
- br plus_cong 1;
-  br refl 1;
- br right_inv2 2;
-br plus_commute 1;
+by (rtac (plus_assoc RS trans) 1);
+by (rtac trans 1);
+ by (rtac plus_cong 1);
+  by (rtac refl 1);
+ by (rtac right_inv2 2);
+by (rtac plus_commute 1);
 val lemma = result();
 bind_thm("minus_plusL3",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
 
diff -r 84c2178db936 -r e65b60b28341 src/HOL/Integ/IntRing.ML
--- a/src/HOL/Integ/IntRing.ML	Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOL/Integ/IntRing.ML	Wed Apr 23 11:02:19 1997 +0200
@@ -14,5 +14,5 @@
 \  sq(i1*j2 + i2*j1 + i3*j4 - i4*j3)  + \
 \  sq(i1*j3 - i2*j4 + i3*j1 + i4*j2)  + \
 \  sq(i1*j4 + i2*j3 - i3*j2 + i4*j1)";
-br Lagrange_lemma 1;
+by (rtac Lagrange_lemma 1);
 qed "Lagrange_lemma_int";
diff -r 84c2178db936 -r e65b60b28341 src/HOL/Integ/Ring.ML
--- a/src/HOL/Integ/Ring.ML	Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOL/Integ/Ring.ML	Wed Apr 23 11:02:19 1997 +0200
@@ -17,123 +17,123 @@
 Addsimps [times_assoc,times_commute,distribL,distribR];
 
 goal Ring.thy "!!x::'a::cring. x*(y*z)=y*(x*z)";
-br trans 1;
-br times_commute 1;
-br trans 1;
-br times_assoc 1;
-by(Simp_tac 1);
+by (rtac trans 1);
+by (rtac times_commute 1);
+by (rtac trans 1);
+by (rtac times_assoc 1);
+by (Simp_tac 1);
 qed "times_commuteL";
 Addsimps [times_commuteL];
 
 val times_cong = read_instantiate [("f1","op *")] (arg_cong RS cong);
 
 goal Ring.thy "!!x::'a::ring. zero*x = zero";
-br trans 1;
- br right_inv 2;
-br trans 1;
- br plus_cong 2;
-  br refl 3;
- br trans 2;
-  br times_cong 3;
-   br zeroL 3;
-  br refl 3;
- br (distribR RS sym) 2;
-br trans 1;
+by (rtac trans 1);
+ by (rtac right_inv 2);
+by (rtac trans 1);
+ by (rtac plus_cong 2);
+  by (rtac refl 3);
+ by (rtac trans 2);
+  by (rtac times_cong 3);
+   by (rtac zeroL 3);
+  by (rtac refl 3);
+ by (rtac (distribR RS sym) 2);
+by (rtac trans 1);
  br(plus_assoc RS sym) 2;
-br trans 1;
- br plus_cong 2;
-  br refl 2;
- br (right_inv RS sym) 2;
-br (zeroR RS sym) 1;
+by (rtac trans 1);
+ by (rtac plus_cong 2);
+  by (rtac refl 2);
+ by (rtac (right_inv RS sym) 2);
+by (rtac (zeroR RS sym) 1);
 qed "mult_zeroL";
 
 goal Ring.thy "!!x::'a::ring. x*zero = zero";
-br trans 1;
- br right_inv 2;
-br trans 1;
- br plus_cong 2;
-  br refl 3;
- br trans 2;
-  br times_cong 3;
-   br zeroL 4;
-  br refl 3;
- br (distribL RS sym) 2;
-br trans 1;
+by (rtac trans 1);
+ by (rtac right_inv 2);
+by (rtac trans 1);
+ by (rtac plus_cong 2);
+  by (rtac refl 3);
+ by (rtac trans 2);
+  by (rtac times_cong 3);
+   by (rtac zeroL 4);
+  by (rtac refl 3);
+ by (rtac (distribL RS sym) 2);
+by (rtac trans 1);
  br(plus_assoc RS sym) 2;
-br trans 1;
- br plus_cong 2;
-  br refl 2;
- br (right_inv RS sym) 2;
-br (zeroR RS sym) 1;
+by (rtac trans 1);
+ by (rtac plus_cong 2);
+  by (rtac refl 2);
+ by (rtac (right_inv RS sym) 2);
+by (rtac (zeroR RS sym) 1);
 qed "mult_zeroR";
 
 goal Ring.thy "!!x::'a::ring. (zero-x)*y = zero-(x*y)";
-br trans 1;
- br zeroL 2;
-br trans 1;
- br plus_cong 2;
-  br refl 3;
- br mult_zeroL 2;
-br trans 1;
- br plus_cong 2;
-  br refl 3;
- br times_cong 2;
-  br left_inv 2;
- br refl 2;
-br trans 1;
- br plus_cong 2;
-  br refl 3;
- br (distribR RS sym) 2;
-br trans 1;
+by (rtac trans 1);
+ by (rtac zeroL 2);
+by (rtac trans 1);
+ by (rtac plus_cong 2);
+  by (rtac refl 3);
+ by (rtac mult_zeroL 2);
+by (rtac trans 1);
+ by (rtac plus_cong 2);
+  by (rtac refl 3);
+ by (rtac times_cong 2);
+  by (rtac left_inv 2);
+ by (rtac refl 2);
+by (rtac trans 1);
+ by (rtac plus_cong 2);
+  by (rtac refl 3);
+ by (rtac (distribR RS sym) 2);
+by (rtac trans 1);
  br(plus_assoc RS sym) 2;
-br trans 1;
- br plus_cong 2;
-  br refl 2;
- br (right_inv RS sym) 2;
-br (zeroR RS sym) 1;
+by (rtac trans 1);
+ by (rtac plus_cong 2);
+  by (rtac refl 2);
+ by (rtac (right_inv RS sym) 2);
+by (rtac (zeroR RS sym) 1);
 qed "mult_invL";
 
 goal Ring.thy "!!x::'a::ring. x*(zero-y) = zero-(x*y)";
-br trans 1;
- br zeroL 2;
-br trans 1;
- br plus_cong 2;
-  br refl 3;
- br mult_zeroR 2;
-br trans 1;
- br plus_cong 2;
-  br refl 3;
- br times_cong 2;
-  br refl 2;
- br left_inv 2;
-br trans 1;
- br plus_cong 2;
-  br refl 3;
- br (distribL RS sym) 2;
-br trans 1;
+by (rtac trans 1);
+ by (rtac zeroL 2);
+by (rtac trans 1);
+ by (rtac plus_cong 2);
+  by (rtac refl 3);
+ by (rtac mult_zeroR 2);
+by (rtac trans 1);
+ by (rtac plus_cong 2);
+  by (rtac refl 3);
+ by (rtac times_cong 2);
+  by (rtac refl 2);
+ by (rtac left_inv 2);
+by (rtac trans 1);
+ by (rtac plus_cong 2);
+  by (rtac refl 3);
+ by (rtac (distribL RS sym) 2);
+by (rtac trans 1);
  br(plus_assoc RS sym) 2;
-br trans 1;
- br plus_cong 2;
-  br refl 2;
- br (right_inv RS sym) 2;
-br (zeroR RS sym) 1;
+by (rtac trans 1);
+ by (rtac plus_cong 2);
+  by (rtac refl 2);
+ by (rtac (right_inv RS sym) 2);
+by (rtac (zeroR RS sym) 1);
 qed "mult_invR";
 
 Addsimps[mult_invL,mult_invR];
 
 
 goal Ring.thy "!!x::'a::ring. x*(y-z) = x*y - x*z";
-by(stac minus_inv 1);
-br sym 1;
-by(stac minus_inv 1);
-by(Simp_tac 1);
+by (stac minus_inv 1);
+by (rtac sym 1);
+by (stac minus_inv 1);
+by (Simp_tac 1);
 qed "minus_distribL";
 
 goal Ring.thy "!!x::'a::ring. (x-y)*z = x*z - y*z";
-by(stac minus_inv 1);
-br sym 1;
-by(stac minus_inv 1);
-by(Simp_tac 1);
+by (stac minus_inv 1);
+by (rtac sym 1);
+by (stac minus_inv 1);
+by (Simp_tac 1);
 qed "minus_distribR";
 
 Addsimps [minus_distribL,minus_distribR];
diff -r 84c2178db936 -r e65b60b28341 src/HOL/MiniML/Generalize.ML
--- a/src/HOL/MiniML/Generalize.ML	Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOL/MiniML/Generalize.ML	Wed Apr 23 11:02:19 1997 +0200
@@ -87,31 +87,31 @@
 qed_spec_mp "gen_subst_commutes";
 
 goal Generalize.thy "free_tv(t::typ) <= free_tv(A) --> bound_typ_inst S (gen A t) = t";
-by(typ.induct_tac "t" 1);
-by(ALLGOALS Asm_simp_tac);
-by(Fast_tac 1);
+by (typ.induct_tac "t" 1);
+by (ALLGOALS Asm_simp_tac);
+by (Fast_tac 1);
 qed_spec_mp "bound_typ_inst_gen";
 Addsimps [bound_typ_inst_gen];
 
 goalw Generalize.thy [le_type_scheme_def,is_bound_typ_instance]
   "gen ($ S A) ($ S t) <= $ S (gen A t)";
-by(safe_tac (!claset));
-by(rename_tac "R" 1);
-by(res_inst_tac [("x", "(%a. bound_typ_inst R (gen ($S A) (S a)))")] exI 1);
-by(typ.induct_tac "t" 1);
- by(simp_tac (!simpset setloop (split_tac[expand_if])) 1);
-by(Asm_simp_tac 1);
+by (safe_tac (!claset));
+by (rename_tac "R" 1);
+by (res_inst_tac [("x", "(%a. bound_typ_inst R (gen ($S A) (S a)))")] exI 1);
+by (typ.induct_tac "t" 1);
+ by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+by (Asm_simp_tac 1);
 qed "gen_bound_typ_instance";
 
 goalw Generalize.thy [le_type_scheme_def,is_bound_typ_instance]
   "!!A B. free_tv B <= free_tv A ==> gen A t <= gen B t";
-by(safe_tac (!claset));
-by(rename_tac "S" 1);
-by(res_inst_tac [("x","%b. if b:free_tv A then TVar b else S b")] exI 1);
+by (safe_tac (!claset));
+by (rename_tac "S" 1);
+by (res_inst_tac [("x","%b. if b:free_tv A then TVar b else S b")] exI 1);
 by (typ.induct_tac "t" 1);
- by(asm_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
- by(Fast_tac 1);
-by(Asm_simp_tac 1);
+ by (asm_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+ by (Fast_tac 1);
+by (Asm_simp_tac 1);
 qed "free_tv_subset_gen_le";
 
 goalw thy [le_type_scheme_def,is_bound_typ_instance] 
@@ -127,7 +127,7 @@
 by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 by (subgoal_tac "n <= n + nat" 1);
 by (forw_inst_tac [("t","A")] new_tv_le 1);
-ba 1;
+by (assume_tac 1);
 by (dtac new_tv_not_free_tv 1);
 by (dtac new_tv_not_free_tv 1);
 by (asm_simp_tac (!simpset addsimps [diff_add_inverse]) 1);
diff -r 84c2178db936 -r e65b60b28341 src/HOL/MiniML/Instance.ML
--- a/src/HOL/MiniML/Instance.ML	Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOL/MiniML/Instance.ML	Wed Apr 23 11:02:19 1997 +0200
@@ -70,7 +70,7 @@
 by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 by (strip_tac 1);
 by (dres_inst_tac [("x","x")] bspec 1);
-ba 1;
+by (assume_tac 1);
 by (dres_inst_tac [("x","x")] bspec 1);
 by (Asm_simp_tac 1);
 by (Asm_full_simp_tac 1);
@@ -110,7 +110,7 @@
 by (cut_inst_tac [("sch","sch")] fresh_variable_type_schemes 1); 
 by (cut_inst_tac [("sch","sch'")] fresh_variable_type_schemes 1);
 by (dtac make_one_new_out_of_two 1);
-ba 1;
+by (assume_tac 1);
 by (thin_tac "? n. new_tv n sch'" 1); 
 by (etac exE 1);
 by (etac allE 1);
@@ -142,7 +142,7 @@
 by (Asm_full_simp_tac 1);
 by (rotate_tac 1 1);
 by (rtac mp 1);
-ba 2;
+by (assume_tac 2);
 by (type_scheme.induct_tac "sch" 1);
 by (Simp_tac 1);
 by (Asm_full_simp_tac 1);
@@ -160,18 +160,18 @@
 
 goalw thy [le_env_def]
   "(sch # A <= sch' # B) = (sch <= (sch'::type_scheme) & A <= B)";
-by(Simp_tac 1);
-br iffI 1;
- by(SELECT_GOAL(safe_tac (!claset))1);
-  by(eres_inst_tac [("x","0")] allE 1);
-  by(Asm_full_simp_tac 1);
- by(eres_inst_tac [("x","Suc i")] allE 1);
- by(Asm_full_simp_tac 1);
-br conjI 1;
- by(Fast_tac 1);
-br allI 1;
-by(nat_ind_tac "i" 1);
-by(ALLGOALS Asm_simp_tac);
+by (Simp_tac 1);
+by (rtac iffI 1);
+ by (SELECT_GOAL(safe_tac (!claset))1);
+  by (eres_inst_tac [("x","0")] allE 1);
+  by (Asm_full_simp_tac 1);
+ by (eres_inst_tac [("x","Suc i")] allE 1);
+ by (Asm_full_simp_tac 1);
+by (rtac conjI 1);
+ by (Fast_tac 1);
+by (rtac allI 1);
+by (nat_ind_tac "i" 1);
+by (ALLGOALS Asm_simp_tac);
 qed "le_env_Cons";
 AddIffs [le_env_Cons];
 
@@ -196,59 +196,59 @@
 qed "S_compatible_le_scheme_lists";
 
 goalw thy [le_type_scheme_def] "!!t.[| t <| sch; sch <= sch' |] ==> t <| sch'";
-by(Fast_tac 1);
+by (Fast_tac 1);
 qed "bound_typ_instance_trans";
 
 goalw thy [le_type_scheme_def] "sch <= (sch::type_scheme)";
-by(Fast_tac 1);
+by (Fast_tac 1);
 qed "le_type_scheme_refl";
 AddIffs [le_type_scheme_refl];
 
 goalw thy [le_env_def] "A <= (A::type_scheme list)";
-by(Fast_tac 1);
+by (Fast_tac 1);
 qed "le_env_refl";
 AddIffs [le_env_refl];
 
 goalw thy [le_type_scheme_def,is_bound_typ_instance] "sch <= BVar n";
-by(strip_tac 1);
-by(res_inst_tac [("x","%a.t")]exI 1);
-by(Simp_tac 1);
+by (strip_tac 1);
+by (res_inst_tac [("x","%a.t")]exI 1);
+by (Simp_tac 1);
 qed "bound_typ_instance_BVar";
 AddIffs [bound_typ_instance_BVar];
 
 goalw thy [le_type_scheme_def,is_bound_typ_instance] "(sch <= FVar n) = (sch = FVar n)";
-by(type_scheme.induct_tac "sch" 1);
-  by(Simp_tac 1);
- by(Simp_tac 1);
- by(SELECT_GOAL(safe_tac(!claset))1);
- by(eres_inst_tac [("x","TVar n -> TVar n")] allE 1);
- by(Asm_full_simp_tac 1);
- by(Fast_tac 1);
-by(Asm_full_simp_tac 1);
-br iffI 1;
- by(eres_inst_tac [("x","bound_typ_inst S type_scheme1 -> bound_typ_inst S type_scheme2")] allE 1);
- by(Asm_full_simp_tac 1);
- by(Fast_tac 1);
-by(Fast_tac 1);
+by (type_scheme.induct_tac "sch" 1);
+  by (Simp_tac 1);
+ by (Simp_tac 1);
+ by (SELECT_GOAL(safe_tac(!claset))1);
+ by (eres_inst_tac [("x","TVar n -> TVar n")] allE 1);
+ by (Asm_full_simp_tac 1);
+ by (Fast_tac 1);
+by (Asm_full_simp_tac 1);
+by (rtac iffI 1);
+ by (eres_inst_tac [("x","bound_typ_inst S type_scheme1 -> bound_typ_inst S type_scheme2")] allE 1);
+ by (Asm_full_simp_tac 1);
+ by (Fast_tac 1);
+by (Fast_tac 1);
 qed "le_FVar";
 Addsimps [le_FVar];
 
 goalw thy [le_type_scheme_def,is_bound_typ_instance] "~(FVar n <= sch1 =-> sch2)";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "not_FVar_le_Fun";
 AddIffs [not_FVar_le_Fun];
 
 goalw thy [le_type_scheme_def,is_bound_typ_instance] "~(BVar n <= sch1 =-> sch2)";
-by(Simp_tac 1);
-by(res_inst_tac [("x","TVar n")] exI 1);
-by(Simp_tac 1);
-by(Fast_tac 1);
+by (Simp_tac 1);
+by (res_inst_tac [("x","TVar n")] exI 1);
+by (Simp_tac 1);
+by (Fast_tac 1);
 qed "not_BVar_le_Fun";
 AddIffs [not_BVar_le_Fun];
 
 goalw thy [le_type_scheme_def,is_bound_typ_instance]
   "!!sch1. (sch1 =-> sch2 <= sch1' =-> sch2') ==> sch1 <= sch1' & sch2 <= sch2'";
-by(fast_tac (!claset addss !simpset) 1);
+by (fast_tac (!claset addss !simpset) 1);
 qed "Fun_le_FunD";
 
 goal thy "(sch' <= sch1 =-> sch2) --> (? sch'1 sch'2. sch' = sch'1 =-> sch'2)";
@@ -259,33 +259,33 @@
 qed_spec_mp "scheme_le_Fun";
 
 goal thy "!sch'::type_scheme. sch <= sch' --> free_tv sch' <= free_tv sch";
-by(type_scheme.induct_tac "sch" 1);
-  br allI 1;
-  by(type_scheme.induct_tac "sch'" 1);
-    by(Simp_tac 1);
-   by(Simp_tac 1);
-  by(Simp_tac 1);
- br allI 1;
- by(type_scheme.induct_tac "sch'" 1);
-   by(Simp_tac 1);
-  by(Simp_tac 1);
- by(Simp_tac 1);
-br allI 1;
-by(type_scheme.induct_tac "sch'" 1);
-  by(Simp_tac 1);
- by(Simp_tac 1);
-by(Asm_full_simp_tac 1);
-by(strip_tac 1);
-bd Fun_le_FunD 1;
-by(Fast_tac 1);
+by (type_scheme.induct_tac "sch" 1);
+  by (rtac allI 1);
+  by (type_scheme.induct_tac "sch'" 1);
+    by (Simp_tac 1);
+   by (Simp_tac 1);
+  by (Simp_tac 1);
+ by (rtac allI 1);
+ by (type_scheme.induct_tac "sch'" 1);
+   by (Simp_tac 1);
+  by (Simp_tac 1);
+ by (Simp_tac 1);
+by (rtac allI 1);
+by (type_scheme.induct_tac "sch'" 1);
+  by (Simp_tac 1);
+ by (Simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (strip_tac 1);
+by (dtac Fun_le_FunD 1);
+by (Fast_tac 1);
 qed_spec_mp "le_type_scheme_free_tv";
 
 goal thy "!A::type_scheme list. A <= B --> free_tv B <= free_tv A";
-by(list.induct_tac "B" 1);
- by(Simp_tac 1);
-br allI 1;
-by(list.induct_tac "A" 1);
- by(simp_tac (!simpset addsimps [le_env_def]) 1);
-by(Simp_tac 1);
-by(fast_tac (!claset addDs [le_type_scheme_free_tv]) 1);
+by (list.induct_tac "B" 1);
+ by (Simp_tac 1);
+by (rtac allI 1);
+by (list.induct_tac "A" 1);
+ by (simp_tac (!simpset addsimps [le_env_def]) 1);
+by (Simp_tac 1);
+by (fast_tac (!claset addDs [le_type_scheme_free_tv]) 1);
 qed_spec_mp "le_env_free_tv";
diff -r 84c2178db936 -r e65b60b28341 src/HOL/MiniML/MiniML.ML
--- a/src/HOL/MiniML/MiniML.ML	Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOL/MiniML/MiniML.ML	Wed Apr 23 11:02:19 1997 +0200
@@ -128,7 +128,7 @@
 by (step_tac (!claset) 1);
 by (cut_facts_tac [aux_plus] 1);
 by (dtac new_tv_le 1);
-ba 1;
+by (assume_tac 1);
 by (rotate_tac 1 1);
 by (dtac new_tv_not_free_tv 1);
 by (Fast_tac 1);
@@ -138,7 +138,7 @@
 by (step_tac (!claset) 1);
 by (cut_facts_tac [aux_plus] 1);
 by (dtac new_tv_le 1);
-ba 1;
+by (assume_tac 1);
 by (rotate_tac 1 1);
 by (dtac new_tv_not_free_tv 1);
 by (Fast_tac 1);
@@ -164,7 +164,7 @@
 by (Asm_simp_tac 1);
 by (subgoal_tac "n <= n + nat" 1);
 by (dtac new_tv_le 1);
-ba 1;
+by (assume_tac 1);
 by (dtac new_tv_not_free_tv 1);
 by (dtac new_tv_not_free_tv 1);
 by (asm_simp_tac (!simpset addsimps [diff_add_inverse ]) 1);
@@ -175,12 +175,12 @@
 AddSIs has_type.intrs;
 
 goal thy "!!e. A |- e::t ==> !B. A <= B -->  B |- e::t";
-by(etac has_type.induct 1);
-   by(simp_tac (!simpset addsimps [le_env_def]) 1);
-   by(fast_tac (!claset addEs [bound_typ_instance_trans] addss !simpset) 1);
-  by(Asm_full_simp_tac 1);
- by(Fast_tac 1);
-by(slow_tac (!claset addEs [le_env_free_tv RS free_tv_subset_gen_le]) 1);
+by (etac has_type.induct 1);
+   by (simp_tac (!simpset addsimps [le_env_def]) 1);
+   by (fast_tac (!claset addEs [bound_typ_instance_trans] addss !simpset) 1);
+  by (Asm_full_simp_tac 1);
+ by (Fast_tac 1);
+by (slow_tac (!claset addEs [le_env_free_tv RS free_tv_subset_gen_le]) 1);
 qed_spec_mp "has_type_le_env";
 
 (* has_type is closed w.r.t. substitution *)
@@ -220,7 +220,7 @@
  val o_apply = prove_goalw HOL.thy [o_def] "(f o g) x = f (g x)"
  (fn _ => [rtac refl 1]);
  by (stac (S'_A_eq_S'_alpha_A) 1);
- ba 1;
+ by (assume_tac 1);
 by (stac S_o_alpha_typ 1);
 by (stac gen_subst_commutes 1);
  by (rtac subset_antisym 1);
@@ -242,7 +242,7 @@
 by (rtac has_type_le_env 1);
  by (dtac spec 1);
  by (dtac spec 1);
- ba 1;
+ by (assume_tac 1);
 by (rtac (app_subst_Cons RS subst) 1);
 by (rtac S_compatible_le_scheme_lists 1);
 by (Asm_simp_tac 1);
diff -r 84c2178db936 -r e65b60b28341 src/HOL/MiniML/Type.ML
--- a/src/HOL/MiniML/Type.ML	Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOL/MiniML/Type.ML	Wed Apr 23 11:02:19 1997 +0200
@@ -18,15 +18,15 @@
 
 goal thy "!t'.mk_scheme t = mk_scheme t' --> t=t'";
 by (typ.induct_tac "t" 1);
- br allI 1;
+ by (rtac allI 1);
  by (typ.induct_tac "t'" 1);
-  by(Simp_tac 1);
- by(Asm_full_simp_tac 1);
-br allI 1;
+  by (Simp_tac 1);
+ by (Asm_full_simp_tac 1);
+by (rtac allI 1);
 by (typ.induct_tac "t'" 1);
- by(Simp_tac 1);
-by(Asm_full_simp_tac 1);
-by(Fast_tac 1);
+ by (Simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (Fast_tac 1);
 qed_spec_mp "mk_scheme_injective";
 
 goal thy "!!t. free_tv (mk_scheme t) = free_tv t";
@@ -105,21 +105,21 @@
 
 goalw thy [id_subst_def,new_tv_def,free_tv_subst,dom_def,cod_def]
   "new_tv n id_subst";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "new_tv_id_subst";
 Addsimps[new_tv_id_subst];
 
 goal thy "new_tv n (sch::type_scheme) --> \
 \              $(%k.if k<n then S k else S' k) sch = $S sch";
 by (type_scheme.induct_tac "sch" 1);
-by(ALLGOALS Asm_simp_tac);
+by (ALLGOALS Asm_simp_tac);
 qed "new_if_subst_type_scheme";
 Addsimps [new_if_subst_type_scheme];
 
 goal thy "new_tv n (A::type_scheme list) --> \
 \              $(%k.if k<n then S k else S' k) A = $S A";
 by (list.induct_tac "A" 1);
-by(ALLGOALS Asm_simp_tac);
+by (ALLGOALS Asm_simp_tac);
 qed "new_if_subst_type_scheme_list";
 Addsimps [new_if_subst_type_scheme_list];
 
@@ -253,17 +253,17 @@
 
 goalw thy [free_tv_subst] 
       "!!v. v : cod S ==> v : free_tv S";
-by( fast_tac set_cs 1);
+by ( fast_tac set_cs 1);
 qed "codD";
  
 goalw thy [free_tv_subst,dom_def] 
       "!! x. x ~: free_tv S ==> S x = TVar x";
-by( fast_tac set_cs 1);
+by ( fast_tac set_cs 1);
 qed "not_free_impl_id";
 
 goalw thy [new_tv_def] 
       "!! n. [| new_tv n t; m:free_tv t |] ==> m<n";
-by( fast_tac HOL_cs 1 );
+by ( fast_tac HOL_cs 1 );
 qed "free_tv_le_new_tv";
 
 goalw thy [dom_def,cod_def,UNION_def,Bex_def]
@@ -278,26 +278,26 @@
 
 goal thy 
      "free_tv (S (v::nat)) <= cod S Un {v}";
-by( cut_inst_tac [("P","v:dom S")] excluded_middle 1);
-by( safe_tac (HOL_cs addSIs [subsetI]) );
+by ( cut_inst_tac [("P","v:dom S")] excluded_middle 1);
+by ( safe_tac (HOL_cs addSIs [subsetI]) );
 by (fast_tac (set_cs addss (!simpset addsimps [dom_def])) 1);
 by (fast_tac (set_cs addss (!simpset addsimps [cod_def])) 1);
 qed "free_tv_subst_var";
 
 goal thy 
      "free_tv ($ S (t::typ)) <= cod S Un free_tv t";
-by( typ.induct_tac "t" 1);
+by ( typ.induct_tac "t" 1);
 (* case TVar n *)
-by( simp_tac (!simpset addsimps [free_tv_subst_var]) 1);
+by ( simp_tac (!simpset addsimps [free_tv_subst_var]) 1);
 (* case Fun t1 t2 *)
-by( fast_tac (set_cs addss !simpset) 1);
+by ( fast_tac (set_cs addss !simpset) 1);
 qed "free_tv_app_subst_te";     
 
 goal thy 
      "free_tv ($ S (sch::type_scheme)) <= cod S Un free_tv sch";
-by( type_scheme.induct_tac "sch" 1);
+by ( type_scheme.induct_tac "sch" 1);
 (* case FVar n *)
-by( simp_tac (!simpset addsimps [free_tv_subst_var]) 1);
+by ( simp_tac (!simpset addsimps [free_tv_subst_var]) 1);
 (* case BVar n *)
 by (Simp_tac 1);
 (* case Fun t1 t2 *)
@@ -306,12 +306,12 @@
 
 goal thy 
      "free_tv ($ S (A::type_scheme list)) <= cod S Un free_tv A";
-by( list.induct_tac "A" 1);
+by ( list.induct_tac "A" 1);
 (* case [] *)
 by (Simp_tac 1);
 (* case a#al *)
-by( cut_facts_tac [free_tv_app_subst_type_scheme] 1);
-by( fast_tac (set_cs addss !simpset) 1);
+by ( cut_facts_tac [free_tv_app_subst_type_scheme] 1);
+by ( fast_tac (set_cs addss !simpset) 1);
 qed "free_tv_app_subst_scheme_list";
 
 goalw thy [free_tv_subst,dom_def]
@@ -396,29 +396,29 @@
 goalw thy [new_tv_def]
   "new_tv n S = ((!m. n <= m --> (S m = TVar m)) & \
 \                (! l. l < n --> new_tv n (S l) ))";
-by( safe_tac HOL_cs );
+by ( safe_tac HOL_cs );
 (* ==> *)
-by( fast_tac (HOL_cs addDs [leD] addss (!simpset addsimps [free_tv_subst,dom_def])) 1);
-by( subgoal_tac "m:cod S | S l = TVar l" 1);
-by( safe_tac HOL_cs );
-by(fast_tac (HOL_cs addDs [UnI2] addss (!simpset addsimps [free_tv_subst])) 1);
-by(dres_inst_tac [("P","%x. m:free_tv x")] subst 1 THEN atac 1);
-by(Asm_full_simp_tac 1);
-by(fast_tac (set_cs addss (!simpset addsimps [free_tv_subst,cod_def,dom_def])) 1);
+by ( fast_tac (HOL_cs addDs [leD] addss (!simpset addsimps [free_tv_subst,dom_def])) 1);
+by ( subgoal_tac "m:cod S | S l = TVar l" 1);
+by ( safe_tac HOL_cs );
+by (fast_tac (HOL_cs addDs [UnI2] addss (!simpset addsimps [free_tv_subst])) 1);
+by (dres_inst_tac [("P","%x. m:free_tv x")] subst 1 THEN atac 1);
+by (Asm_full_simp_tac 1);
+by (fast_tac (set_cs addss (!simpset addsimps [free_tv_subst,cod_def,dom_def])) 1);
 (* <== *)
-by( rewrite_goals_tac [free_tv_subst,cod_def,dom_def] );
-by( safe_tac set_cs );
-by( cut_inst_tac [("m","m"),("n","n")] less_linear 1);
-by( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
-by( cut_inst_tac [("m","ma"),("n","n")] less_linear 1);
-by( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
+by ( rewrite_goals_tac [free_tv_subst,cod_def,dom_def] );
+by ( safe_tac set_cs );
+by ( cut_inst_tac [("m","m"),("n","n")] less_linear 1);
+by ( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
+by ( cut_inst_tac [("m","ma"),("n","n")] less_linear 1);
+by ( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
 qed "new_tv_subst";
 
 goal thy 
   "new_tv n  = list_all (new_tv n)";
 by (rtac ext 1);
-by(list.induct_tac "x" 1);
-by(ALLGOALS Asm_simp_tac);
+by (list.induct_tac "x" 1);
+by (ALLGOALS Asm_simp_tac);
 qed "new_tv_list";
 
 (* substitution affects only variables occurring freely *)
@@ -501,7 +501,7 @@
 
 goal thy
   "new_tv n A --> new_tv (Suc n) ((TVar n)#A)";
-by( simp_tac (!simpset addsimps [new_tv_list]) 1);
+by ( simp_tac (!simpset addsimps [new_tv_list]) 1);
 by (list.induct_tac "A" 1);
 by (ALLGOALS Asm_full_simp_tac);
 qed "new_tv_Suc_list";
@@ -627,13 +627,13 @@
 by (cut_inst_tac [("t","t")] fresh_variable_types 1);
 by (cut_inst_tac [("t","t'")] fresh_variable_types 1);
 by (dtac make_one_new_out_of_two 1);
-ba 1;
+by (assume_tac 1);
 by (thin_tac "? n. new_tv n t'" 1);
 by (cut_inst_tac [("A","A")] fresh_variable_type_scheme_lists 1);
 by (cut_inst_tac [("A","A'")] fresh_variable_type_scheme_lists 1);
 by (rotate_tac 1 1);
 by (dtac make_one_new_out_of_two 1);
-ba 1;
+by (assume_tac 1);
 by (thin_tac "? n. new_tv n A'" 1);
 by (REPEAT (etac exE 1));
 by (rename_tac "n2 n1" 1);
@@ -646,14 +646,14 @@
 goalw thy [new_tv_def] 
       "!! n. [|mgu t1 t2 = Some u; new_tv n t1; new_tv n t2|] ==> \
 \            new_tv n u";
-by( fast_tac (set_cs addDs [mgu_free]) 1);
+by ( fast_tac (set_cs addDs [mgu_free]) 1);
 qed "mgu_new";
 
 
 (* lemmata for substitutions *)
 
 goalw Type.thy [app_subst_list] "length ($ S A) = length A";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "length_app_subst_list";
 Addsimps [length_app_subst_list];
 
@@ -714,8 +714,8 @@
 
 (* composition of substitutions *)
 goalw Type.thy [id_subst_def,o_def] "$S o id_subst = S";
-br ext 1;
-by(Simp_tac 1);
+by (rtac ext 1);
+by (Simp_tac 1);
 qed "o_id_subst";
 Addsimps[o_id_subst];
 
@@ -747,7 +747,7 @@
 
 goal thy "!!A::type_scheme list. !x : free_tv A. S x = (TVar x) ==> $ S A = A";
 by (stac subst_id_on_type_scheme_list' 1);
-ba 1;
+by (assume_tac 1);
 by (Simp_tac 1);
 qed "subst_id_on_type_scheme_list";
 
diff -r 84c2178db936 -r e65b60b28341 src/HOL/MiniML/W.ML
--- a/src/HOL/MiniML/W.ML	Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOL/MiniML/W.ML	Wed Apr 23 11:02:19 1997 +0200
@@ -70,8 +70,8 @@
 goal thy "!! s. new_tv n A ==> Some (S,t,m) = W e A n ==> new_tv m A";
 by (dtac W_var_geD 1);
 by (rtac new_scheme_list_le 1);
-ba 1;
-ba 1;
+by (assume_tac 1);
+by (assume_tac 1);
 qed "new_tv_compatible_W";
 
 goal thy "!!sch. new_tv n sch --> new_tv (n + (min_new_bound_tv sch)) (bound_typ_inst (%b. TVar (b + n)) sch)";
@@ -85,7 +85,7 @@
 by (rtac new_tv_le 1);
 by (mp_tac 2);
 by (mp_tac 2);
-ba 2;
+by (assume_tac 2);
 by (rtac add_le_mono 1);
 by (Simp_tac 1);
 by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [max_def]) 1);
@@ -93,7 +93,7 @@
 by (rtac new_tv_le 1);
 by (mp_tac 2);
 by (mp_tac 2);
-ba 2;
+by (assume_tac 2);
 by (rtac add_le_mono 1);
 by (Simp_tac 1);
 by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [max_def]) 1);
@@ -121,7 +121,7 @@
 by (dtac sym 1);
 by (dtac sym 1);
 by (dtac new_tv_nth_nat_A 1);
-ba 1;
+by (assume_tac 1);
 by (Asm_full_simp_tac 1);
 (* case Abs e *)
 by (simp_tac (!simpset addsimps [new_tv_subst,new_tv_Suc_list] 
@@ -146,7 +146,7 @@
 by (eres_inst_tac [("x","S1")] allE 1);
 by (eres_inst_tac [("x","t1")] allE 1);
 by (eres_inst_tac [("x","n2")] allE 1);
-by( asm_full_simp_tac (!simpset addsimps [o_def,rotate_Some]) 1);
+by ( asm_full_simp_tac (!simpset addsimps [o_def,rotate_Some]) 1);
 by (rtac conjI 1);
 by (rtac new_tv_subst_comp_2 1);
 by (rtac new_tv_subst_comp_2 1);
@@ -203,9 +203,9 @@
 by (rtac new_tv_subst_comp_2 1);
 by (res_inst_tac [("n","n2")] new_tv_subst_le 1);
 by (etac W_var_ge 1);
-ba 1;
-ba 1;
-ba 1;
+by (assume_tac 1);
+by (assume_tac 1);
+by (assume_tac 1);
 by (rewtac new_tv_def);
 by (Asm_simp_tac 1);
 by (dtac W_var_ge 1);
@@ -356,12 +356,12 @@
 by (Asm_full_simp_tac 1);
 by (rtac has_type.AbsI 1);
 by (dtac (le_refl RS le_SucI RS new_scheme_list_le) 1);
-bd sym 1;
+by (dtac sym 1);
 by (REPEAT (etac allE 1));
 by (etac impE 1);
 by (mp_tac 2);
 by (Asm_simp_tac 1);
-ba 1;
+by (assume_tac 1);
 (* case App e1 e2 *)
 by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
 by (strip_tac 1);
@@ -377,23 +377,23 @@
 by (asm_full_simp_tac (!simpset addsimps [subst_comp_scheme_list RS sym,o_def,has_type_cl_sub,eq_sym_conv]) 1);
 by (rtac (has_type_cl_sub RS spec) 1);
 by (forward_tac [new_tv_W] 1);
-ba 1;
+by (assume_tac 1);
 by (dtac conjunct1 1);
 by (dtac conjunct1 1);
 by (forward_tac [new_tv_subst_scheme_list] 1);
 by (rtac new_scheme_list_le 1);
 by (rtac W_var_ge 1);
-ba 1;
-ba 1;
+by (assume_tac 1);
+by (assume_tac 1);
 by (etac thin_rl 1);
 by (REPEAT (etac allE 1));
-bd sym 1;
-bd sym 1;
+by (dtac sym 1);
+by (dtac sym 1);
 by (etac thin_rl 1);
 by (etac thin_rl 1);
 by (mp_tac 1);
 by (mp_tac 1);
-ba 1;
+by (assume_tac 1);
 (* case Let e1 e2 *)
 by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
 by (strip_tac 1);
@@ -421,19 +421,19 @@
 by (dres_inst_tac [("x","n2")] spec 2);
 by (dres_inst_tac [("x","m2")] spec 2);
 by (forward_tac [new_tv_W] 2);
-ba 2;
+by (assume_tac 2);
 by (dtac conjunct1 2);
 by (dtac conjunct1 2);
 by (forward_tac [new_tv_subst_scheme_list] 2);
 by (rtac new_scheme_list_le 2);
 by (rtac W_var_ge 2);
-ba 2;
-ba 2;
+by (assume_tac 2);
+by (assume_tac 2);
 by (etac impE 2);
 by (res_inst_tac [("A","$ S1 A")] new_tv_only_depends_on_free_tv_scheme_list 2);
 by (Simp_tac 2);
 by (Fast_tac 2);
-ba 2;
+by (assume_tac 2);
 by (Asm_full_simp_tac 2);
 by (rtac weaken_A_Int_B_eq_empty 1);
 by (rtac allI 1);
@@ -443,24 +443,24 @@
 by (rtac disjI2 1);
 by (rtac (free_tv_gen_cons RS subst) 1);
 by (rtac free_tv_W 1);
-ba 1;
+by (assume_tac 1);
 by (Asm_full_simp_tac 1);
-ba 1;
+by (assume_tac 1);
 by (rtac disjI1 1);
 by (dtac new_tv_W 1);
-ba 1;
+by (assume_tac 1);
 by (dtac conjunct2 1);
 by (dtac conjunct2 1);
 by (rtac new_tv_not_free_tv 1);
 by (rtac new_tv_le 1);
-ba 2;
+by (assume_tac 2);
 by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le]) 1);
 qed_spec_mp "W_correct_lemma";
 
 goal Arith.thy "!!n::nat. ~ k+n < n";
 by (nat_ind_tac "k" 1);
-by(ALLGOALS Asm_simp_tac);
-by(trans_tac 1);
+by (ALLGOALS Asm_simp_tac);
+by (trans_tac 1);
 val not_add_less1 = result();
 Addsimps [not_add_less1];
 
@@ -567,10 +567,10 @@
 by (fast_tac (HOL_cs addDs [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_W,new_tv_not_free_tv]) 3);
 by (case_tac "na: free_tv t - free_tv Sa" 2);
 (* case na ~: free_tv t - free_tv Sa *)
-by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
+by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
 by (Fast_tac 3);
 (* case na : free_tv t - free_tv Sa *)
-by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
+by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
 by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
 by (dtac eq_subst_scheme_list_eq_free 2);
 by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
@@ -579,21 +579,21 @@
 by (asm_simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1); 
 by (safe_tac HOL_cs );
 by (dtac mgu_Some 1);
-by( fast_tac (HOL_cs addss !simpset) 1);
+by ( fast_tac (HOL_cs addss !simpset) 1);
 (** LEVEL 80 *)
 by ((dtac mgu_mg 1) THEN (atac 1));
 by (etac exE 1);
 by (res_inst_tac [("x","Rb")] exI 1);
 by (rtac conjI 1);
 by (dres_inst_tac [("x","ma")] fun_cong 2);
-by( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2);
+by ( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2);
 by (simp_tac (!simpset addsimps [subst_comp_scheme_list]) 1);
 by (simp_tac (!simpset addsimps [subst_comp_scheme_list RS sym]) 1);
 by (res_inst_tac [("A2","($ Sa ($ S A))")]
        ((subst_comp_scheme_list RS sym) RSN (2,trans)) 1);
-by( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1);
+by ( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1);
 by (rtac eq_free_eq_subst_scheme_list 1);
-by( safe_tac HOL_cs );
+by ( safe_tac HOL_cs );
 by (subgoal_tac "ma ~= na" 1);
 by ((forward_tac [new_tv_W] 2) THEN (atac 2));
 by (etac conjE 2);
@@ -632,13 +632,13 @@
 by (Asm_full_simp_tac 1);
 by (dtac mp 1);
 by (rtac has_type_le_env 1);
-ba 1;
+by (assume_tac 1);
 by (Simp_tac 1);
 by (rtac gen_bound_typ_instance 1);
 by (dtac mp 1);
 by (forward_tac [new_tv_compatible_W] 1);
 by (rtac sym 1);
-ba 1;
+by (assume_tac 1);
 by (fast_tac (!claset addDs [new_tv_compatible_gen,new_tv_subst_scheme_list,new_tv_W]) 1);
 by (safe_tac HOL_cs);
 by (Asm_full_simp_tac 1);
@@ -649,7 +649,7 @@
 goal W.thy
  "!!e. [] |- e :: t' ==>  (? S t. (? m. W e [] n = Some(S,t,m)) &  \
 \                                 (? R. t' = $ R t))";
-by(cut_inst_tac [("A","[]"),("S'","id_subst"),("e","e"),("t'","t'")]
+by (cut_inst_tac [("A","[]"),("S'","id_subst"),("e","e"),("t'","t'")]
                 W_complete_lemma 1);
-by(ALLGOALS Asm_full_simp_tac);
+by (ALLGOALS Asm_full_simp_tac);
 qed "W_complete";
diff -r 84c2178db936 -r e65b60b28341 src/HOL/W0/W.ML
--- a/src/HOL/W0/W.ML	Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOL/W0/W.ML	Wed Apr 23 11:02:19 1997 +0200
@@ -19,7 +19,7 @@
 by (asm_full_simp_tac (!simpset addsimps [app_subst_list]
                         setloop (split_tac [expand_bind])) 1);
 by (strip_tac 1);
-bd sym 1;
+by (dtac sym 1);
 by (fast_tac (HOL_cs addss !simpset) 1);
 (* case App e1 e2 *)
 by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
diff -r 84c2178db936 -r e65b60b28341 src/HOL/ex/LFilter.ML
--- a/src/HOL/ex/LFilter.ML	Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOL/ex/LFilter.ML	Wed Apr 23 11:02:19 1997 +0200
@@ -19,13 +19,13 @@
 
 
 goal thy "!!p. (l,l'): findRel p ==> (l,l''): findRel p --> l'' = l'";
-be findRel.induct 1;
+by (etac findRel.induct 1);
 by (Blast_tac 1);
 by (Blast_tac 1);
 qed_spec_mp "findRel_functional";
 
 goal thy "!!p. (l,l'): findRel p ==> EX x l''. l' = LCons x l'' & p x";
-be findRel.induct 1;
+by (etac findRel.induct 1);
 by (Blast_tac 1);
 by (Blast_tac 1);
 qed_spec_mp "findRel_imp_LCons";
@@ -50,7 +50,7 @@
 goal thy "[| l: Domain (findRel p);                                   \
 \            !!x l'. [| (l, LCons x l') : findRel p;  p x |] ==> Q    \
 \         |] ==> Q";
-br (major RS DomainE) 1;
+by (rtac (major RS DomainE) 1);
 by (forward_tac [findRel_imp_LCons] 1);
 by (REPEAT (eresolve_tac [exE,conjE] 1));
 by (hyp_subst_tac 1);
@@ -60,7 +60,7 @@
 val prems = goal thy
     "[| !!x. p x ==> q x |] ==> Domain (findRel p) <= Domain (findRel q)";
 by (Step_tac 1);
-be findRel.induct 1;
+by (etac findRel.induct 1);
 by (blast_tac (!claset addIs (findRel.intrs@prems)) 1);
 by (blast_tac (!claset addIs findRel.intrs) 1);
 qed "Domain_findRel_mono";
@@ -96,7 +96,7 @@
 
 goal thy "find p (LCons x l) = (if p x then LCons x l else find p l)";
 by (asm_simp_tac (!simpset addsimps [find_LCons_found, find_LCons_seek]
-		           setloop split_tac[expand_if]) 1);
+                           setloop split_tac[expand_if]) 1);
 qed "find_LCons";
 
 
@@ -130,18 +130,18 @@
 by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
 by (case_tac "LCons x l : Domain(findRel p)" 1);
 by (asm_full_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
-be Domain_findRelE 1;
+by (etac Domain_findRelE 1);
 by (safe_tac (!claset delrules [conjI]));
 by (asm_full_simp_tac 
     (!simpset addsimps [findRel_imp_lfilter, findRel_imp_find,
-			find_LCons_seek]) 1);
+                        find_LCons_seek]) 1);
 qed "lfilter_LCons_seek";
 
 
 goal thy "lfilter p (LCons x l) = \
 \         (if p x then LCons x (lfilter p l) else lfilter p l)";
 by (asm_simp_tac (!simpset addsimps [lfilter_LCons_found, lfilter_LCons_seek]
-		           setloop split_tac[expand_if]) 1);
+                           setloop split_tac[expand_if]) 1);
 qed "lfilter_LCons";
 
 AddSIs [llistD_Fun_LNil_I, llistD_Fun_LCons_I];
@@ -149,9 +149,9 @@
 
 
 goal thy "!!p. lfilter p l = LNil ==> l ~: Domain(findRel p)";
-br notI 1;
-be Domain_findRelE 1;
-be rev_mp 1;
+by (rtac notI 1);
+by (etac Domain_findRelE 1);
+by (etac rev_mp 1);
 by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
 qed "lfilter_eq_LNil";
 
@@ -160,7 +160,7 @@
 \              (EX l''. l' = lfilter p l'' & (l, LCons x l'') : findRel p)";
 by (stac (lfilter_def RS def_llist_corec) 1);
 by (case_tac "l : Domain(findRel p)" 1);
-be Domain_findRelE 1;
+by (etac Domain_findRelE 1);
 by (Asm_simp_tac 2);
 by (asm_simp_tac (!simpset addsimps [findRel_imp_find]) 1);
 by (Blast_tac 1);
@@ -190,8 +190,8 @@
 by (Step_tac 1);
 (*Cases: p x is true or false*)
 by (Blast_tac 1);
-br (lfilter_cases RS disjE) 1;
-be ssubst 1;
+by (rtac (lfilter_cases RS disjE) 1);
+by (etac ssubst 1);
 by (Auto_tac());
 qed "lfilter_idem";
 
@@ -202,7 +202,7 @@
 
 goal thy "!!p. (l,l') : findRel q \
 \           ==> l' = LCons x l'' --> p x --> (l,l') : findRel (%x. p x & q x)";
-be findRel.induct 1;
+by (etac findRel.induct 1);
 by (blast_tac (!claset addIs findRel.intrs) 1);
 by (blast_tac (!claset addIs findRel.intrs) 1);
 qed_spec_mp "findRel_conj_lemma";
@@ -212,7 +212,7 @@
 goal thy "!!p. (l,l'') : findRel (%x. p x & q x) \
 \              ==> (l, LCons x l') : findRel q --> ~ p x     \
 \                  --> l' : Domain (findRel (%x. p x & q x))";
-be findRel.induct 1;
+by (etac findRel.induct 1);
 by (Auto_tac());
 qed_spec_mp "findRel_not_conj_Domain";
 
@@ -220,7 +220,7 @@
 goal thy "!!p. (l,lxx) : findRel q ==> \
 \            lxx = LCons x lx --> (lx,lz) : findRel(%x. p x & q x) --> ~ p x \
 \            --> (l,lz) : findRel (%x. p x & q x)";
-be findRel.induct 1;
+by (etac findRel.induct 1);
 by (ALLGOALS (blast_tac (!claset addIs findRel.intrs)));
 qed_spec_mp "findRel_conj2";
 
@@ -228,14 +228,14 @@
 goal thy "!!p. (lx,ly) : findRel p \
 \              ==> ALL l. lx = lfilter q l \
 \                  --> l : Domain (findRel(%x. p x & q x))";
-be findRel.induct 1;
+by (etac findRel.induct 1);
 by (blast_tac (!claset addSDs [sym RS lfilter_eq_LCons]
-	               addIs  [findRel_conj]) 1);
+                       addIs  [findRel_conj]) 1);
 by (Auto_tac());
-bd (sym RS lfilter_eq_LCons) 1;
+by (dtac (sym RS lfilter_eq_LCons) 1);
 by (Auto_tac());
-bd spec 1;
-bd (refl RS rev_mp) 1;
+by (dtac spec 1);
+by (dtac (refl RS rev_mp) 1);
 by (blast_tac (!claset addIs [findRel_conj2]) 1);
 qed_spec_mp "findRel_lfilter_Domain_conj";
 
@@ -243,7 +243,7 @@
 goal thy "!!p. (l,l'') : findRel(%x. p x & q x) \
 \              ==> l'' = LCons y l' --> \
 \                  (lfilter q l, LCons y (lfilter q l')) : findRel p";
-be findRel.induct 1;
+by (etac findRel.induct 1);
 by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac[expand_if])));
 by (ALLGOALS (blast_tac (!claset addIs findRel.intrs)));
 qed_spec_mp "findRel_conj_lfilter";
@@ -263,7 +263,7 @@
 (*case q x*)
 by (case_tac "p x" 1);
 by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter,
-				     findRel_conj RS findRel_imp_lfilter]) 1);
+                                     findRel_conj RS findRel_imp_lfilter]) 1);
 by (Blast_tac 1);
 (*case q x and ~(p x) *)
 by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
@@ -276,7 +276,7 @@
 (*    ...and therefore too, no p in lfilter q l'.  Both results are Lnil*)
 by (asm_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
 (*subcase: there is a p&q in l' and therefore also one in l*)
-be Domain_findRelE 1;
+by (etac Domain_findRelE 1);
 by (subgoal_tac "(l, LCons xa l'a) : findRel(%x. p x & q x)" 1);
 by (blast_tac (!claset addIs [findRel_conj2]) 2);
 by (subgoal_tac "(lfilter q l', LCons xa (lfilter q l'a)) : findRel p" 1);
@@ -298,7 +298,7 @@
  ***)
 
 goal thy "!!p. (l,l') : findRel(%x. p (f x)) ==> lmap f l : Domain(findRel p)";
-be findRel.induct 1;
+by (etac findRel.induct 1);
 by (ALLGOALS Asm_full_simp_tac);
 qed "findRel_lmap_Domain";
 
@@ -315,7 +315,7 @@
 \    ALL l. lmap f l = lx --> ly = LCons x l' --> \
 \    (EX y l''. x = f y & l' = lmap f l'' &       \
 \    (l, LCons y l'') : findRel(%x. p(f x)))";
-be findRel.induct 1;
+by (etac findRel.induct 1);
 by (ALLGOALS Asm_simp_tac);
 by (safe_tac (!claset addSDs [lmap_eq_LCons]));
 by (blast_tac (!claset addIs findRel.intrs) 1);
@@ -333,7 +333,7 @@
 by (subgoal_tac "l ~: Domain (findRel(%x. p (f x)))" 2);
 by (blast_tac (!claset addIs [findRel_lmap_Domain]) 3);
 by (asm_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
-be Domain_findRelE 1;
+by (etac Domain_findRelE 1);
 by (forward_tac [lmap_LCons_findRel] 1);
 by (Step_tac 1);
 by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
diff -r 84c2178db936 -r e65b60b28341 src/HOL/ex/LList.ML
--- a/src/HOL/ex/LList.ML	Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOL/ex/LList.ML	Wed Apr 23 11:02:19 1997 +0200
@@ -649,7 +649,7 @@
 goalw thy [llistD_Fun_def, prod_fun_def]
     "!!A B. A<=B ==> llistD_Fun A <= llistD_Fun B";
 by (Auto_tac());
-br image_eqI 1;
+by (rtac image_eqI 1);
 by (fast_tac (!claset addss (!simpset)) 1);
 by (blast_tac (!claset addIs [impOfSubs LListD_Fun_mono]) 1);
 qed "llistD_Fun_mono";
diff -r 84c2178db936 -r e65b60b28341 src/HOLCF/Discrete0.ML
--- a/src/HOLCF/Discrete0.ML	Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOLCF/Discrete0.ML	Wed Apr 23 11:02:19 1997 +0200
@@ -7,16 +7,16 @@
 *)
 
 goalw thy [less_discr_def] "less (x::('a::term)discr) x";
-br refl 1;
+by (rtac refl 1);
 qed "less_discr_refl";
 
 goalw thy [less_discr_def]
   "!!x. [| less (x::('a::term)discr) y; less y z |] ==> less x z";
-be trans 1;
-ba 1;
+by (etac trans 1);
+by (assume_tac 1);
 qed "less_discr_trans";
 
 goalw thy [less_discr_def]
   "!!x. [| less (x::('a::term)discr) y; less y x |] ==> x=y";
-ba 1;
+by (assume_tac 1);
 qed "less_discr_antisym";
diff -r 84c2178db936 -r e65b60b28341 src/HOLCF/Discrete1.ML
--- a/src/HOLCF/Discrete1.ML	Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOLCF/Discrete1.ML	Wed Apr 23 11:02:19 1997 +0200
@@ -7,26 +7,26 @@
 *)
 
 goalw thy [po_def,less_discr_def] "((x::('a::term)discr) << y) = (x=y)";
-br refl 1;
+by (rtac refl 1);
 qed "discr_less_eq";
 AddIffs [discr_less_eq];
 
 goalw thy [is_chain]
  "!!S::nat=>('a::term)discr. is_chain S ==> S i = S 0";
-by(nat_ind_tac "i" 1);
- br refl 1;
-be subst 1;
-br sym 1;
-by(Fast_tac 1);
+by (nat_ind_tac "i" 1);
+ by (rtac refl 1);
+by (etac subst 1);
+by (rtac sym 1);
+by (Fast_tac 1);
 qed "discr_chain0";
 
 goal thy
  "!!S::nat=>('a::term)discr. is_chain(S) ==> range(S) = {S 0}";
-by(fast_tac (!claset addEs [discr_chain0]) 1);
+by (fast_tac (!claset addEs [discr_chain0]) 1);
 qed "discr_chain_range0";
 Addsimps [discr_chain_range0];
 
 goalw thy [is_lub,is_ub]
  "!!S. is_chain S ==> ? x::('a::term)discr. range(S) <<| x";
-by(Asm_simp_tac 1);
+by (Asm_simp_tac 1);
 qed "discr_cpo";
diff -r 84c2178db936 -r e65b60b28341 src/HOLCF/Porder.ML
--- a/src/HOLCF/Porder.ML	Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOLCF/Porder.ML	Wed Apr 23 11:02:19 1997 +0200
@@ -137,8 +137,8 @@
 
 
 goal thy "lub{x} = x";
-br thelubI 1;
-by(simp_tac (!simpset addsimps [is_lub,is_ub]) 1);
+by (rtac thelubI 1);
+by (simp_tac (!simpset addsimps [is_lub,is_ub]) 1);
 qed "lub_singleton";
 Addsimps [lub_singleton];
 
diff -r 84c2178db936 -r e65b60b28341 src/HOLCF/ex/Focus_ex.ML
--- a/src/HOLCF/ex/Focus_ex.ML	Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOLCF/ex/Focus_ex.ML	Wed Apr 23 11:02:19 1997 +0200
@@ -75,7 +75,7 @@
 by (strip_tac 1);
 by (rtac fix_least 1);
 by (Simp_tac 1);
-by(etac exE 1);
+by (etac exE 1);
 by (dtac sym 1);
 back();
 by (asm_simp_tac HOLCF_ss 1);
@@ -84,7 +84,7 @@
 (* direction is_g(g) --> def_g(g) *)
 val prems = goal Focus_ex.thy "is_g(g) --> def_g(g)";
 by (simp_tac (HOL_ss delsimps (ex_simps @ all_simps)
-		     addsimps [lemma1,lemma2,def_g]) 1);
+                     addsimps [lemma1,lemma2,def_g]) 1);
 by (rtac impI 1);
 by (etac exE 1);
 by (res_inst_tac [("x","f")] exI 1);