src/HOL/MiniML/Instance.ML

 by (safe_tac (!claset));
 by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 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);
 qed_spec_mp "bound_scheme_inst_type";
 

       "!!(sch::type_scheme) sch'. (sch' <= sch) = (? B. sch' = bound_scheme_inst B sch)";
 by (rtac iffI 1);
 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);
 by (dtac mp 1);
 by (res_inst_tac [("x","(%k. TVar (k + n))")] exI 1);

 by (rtac exI 1);
 by (rtac mk_scheme_injective 1); 
 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);
 by (Fast_tac 1);
 by (strip_tac 1);

 by (Asm_full_simp_tac 1);
 qed_spec_mp "le_type_eq_is_bound_typ_instance";
 
 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];
 
 goalw thy [is_bound_typ_instance]"!!t. t <| sch ==> $S t <| $S sch";
 by (etac exE 1);

 by (simp_tac (!simpset addcongs [conj_cong]) 1);
 by (fast_tac (!claset addSIs [S_compatible_le_scheme]) 1);
 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)";
 by (type_scheme.induct_tac "sch'" 1);
 by (Asm_simp_tac 1);
 by (Asm_simp_tac 1);
 by (Fast_tac 1);
 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";