1.1 --- a/src/HOL/Induct/Acc.ML	Tue Jul 21 08:54:09 1998 +0200
     1.2 +++ b/src/HOL/Induct/Acc.ML	Tue Jul 21 12:12:52 1998 +0200
     1.3 @@ -25,12 +25,12 @@
     1.4  qed "acc_downward";
     1.5  
     1.6  Goal "(b,a) : r^* ==> a : acc r --> b : acc r";
     1.7 -be rtrancl_induct 1;
     1.8 -by(Blast_tac 1);
     1.9 - by(blast_tac (claset() addDs [acc_downward]) 1);
    1.10 +by (etac rtrancl_induct 1);
    1.11 +by (Blast_tac 1);
    1.12 + by (blast_tac (claset() addDs [acc_downward]) 1);
    1.13  val lemma = result();
    1.14  Goal "[| a : acc r; (b,a) : r^* |] ==> b : acc r";
    1.15 -by(blast_tac (claset() addDs [lemma]) 1);
    1.16 +by (blast_tac (claset() addDs [lemma]) 1);
    1.17  qed "acc_downwards";
    1.18  
    1.19  val [major,indhyp] = goal Acc.thy

     2.1 --- a/src/HOL/Lambda/ParRed.ML	Tue Jul 21 08:54:09 1998 +0200
     2.2 +++ b/src/HOL/Lambda/ParRed.ML	Tue Jul 21 12:12:52 1998 +0200
     2.3 @@ -83,9 +83,9 @@
     2.4  Addsimps cd.rules;
     2.5  
     2.6  Goal "!t. s => t --> t => cd s";
     2.7 -by(res_inst_tac[("u","s")] cd.induct 1);
     2.8 -by(Auto_tac);
     2.9 -by(fast_tac (claset() addSIs [par_beta_subst]) 1);
    2.10 +by (res_inst_tac[("u","s")] cd.induct 1);
    2.11 +by (Auto_tac);
    2.12 +by (fast_tac (claset() addSIs [par_beta_subst]) 1);
    2.13  qed_spec_mp "par_beta_cd";
    2.14  
    2.15  (*** Confluence (via cd) ***)

     3.1 --- a/src/HOL/Lex/MaxChop.ML	Tue Jul 21 08:54:09 1998 +0200
     3.2 +++ b/src/HOL/Lex/MaxChop.ML	Tue Jul 21 12:12:52 1998 +0200
     3.3 @@ -83,8 +83,8 @@
     3.4  by (simp_tac (simpset() addsimps [Let_def,rewrite_rule[is_maxsplitter_def]prem]
     3.5                          addsplits [split_split]) 1);
     3.6  by (Clarify_tac 1);
     3.7 -by(rename_tac "xs1 ys1 xss1 ys" 1);
     3.8 -by(split_asm_tac [split_list_case_asm] 1);
     3.9 +by (rename_tac "xs1 ys1 xss1 ys" 1);
    3.10 +by (split_asm_tac [split_list_case_asm] 1);
    3.11   by (Asm_full_simp_tac 1);
    3.12   by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
    3.13   by (blast_tac (claset() addIs [prefix_append RS iffD2]) 1);
    3.14 @@ -93,7 +93,7 @@
    3.15   by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
    3.16   by (blast_tac (claset() addIs [prefix_append RS iffD2]) 1);
    3.17  by (Clarify_tac 1);
    3.18 -by(rename_tac "us uss" 1);
    3.19 +by (rename_tac "us uss" 1);
    3.20  by (subgoal_tac "xs1=us" 1);
    3.21   by (Asm_full_simp_tac 1);
    3.22  by (Asm_full_simp_tac 1);

     4.1 --- a/src/ZF/Update.ML	Tue Jul 21 08:54:09 1998 +0200
     4.2 +++ b/src/ZF/Update.ML	Tue Jul 21 12:12:52 1998 +0200
     4.3 @@ -20,7 +20,7 @@
     4.4  by (asm_simp_tac (simpset() addsimps [domain_of_fun, cons_absorb]) 1);
     4.5  by (rtac fun_extension 1);
     4.6  by (best_tac (claset() addIs [apply_type, if_type, lam_type]) 1);
     4.7 -ba 1;
     4.8 +by (assume_tac 1);
     4.9  by (Asm_simp_tac 1);
    4.10  qed "update_idem";
    4.11  

     5.1 --- a/src/ZF/ex/Integ.ML	Tue Jul 21 08:54:09 1998 +0200
     5.2 +++ b/src/ZF/ex/Integ.ML	Tue Jul 21 12:12:52 1998 +0200
     5.3 @@ -140,7 +140,7 @@
     5.4  
     5.5  Goalw [znegative_def, znat_def] "n: nat ==> znegative($~ $# succ(n))";
     5.6  by (asm_simp_tac (simpset() addsimps [zminus]) 1);
     5.7 -by(blast_tac (claset() addIs [nat_0_le]) 1);
     5.8 +by (blast_tac (claset() addIs [nat_0_le]) 1);
     5.9  qed "znegative_zminus_znat";
    5.10  
    5.11