1.1 --- a/src/HOL/Lex/RegExp2NAe.ML	Wed Aug 19 10:27:25 1998 +0200
     1.2 +++ b/src/HOL/Lex/RegExp2NAe.ML	Wed Aug 19 10:27:49 1998 +0200
     1.3 @@ -211,28 +211,9 @@
     1.4  by (Clarify_tac 1);
     1.5  by (rtac compI 1);
     1.6  by (rtac compI 1);
     1.7 -by (rtac (epsclosure_start_step_union RS iffD2) 1);
     1.8 -by (rtac disjI2 1);
     1.9 -by (rtac exI 1);
    1.10 -by (rtac conjI 1);
    1.11 -by (rtac (start_eps_union RS iffD2) 1);
    1.12 -by (rtac disjI2 1);
    1.13 -by (rtac refl 1);
    1.14 -by (Clarify_tac 1);
    1.15 -by (rtac exI 1);
    1.16 -by (rtac conjI 1);
    1.17 -by (rtac refl 1);
    1.18 -by (assume_tac 1);
    1.19 -by (Clarify_tac 1);
    1.20 -by (rtac exI 1);
    1.21 -by (rtac conjI 1);
    1.22 -by (rtac refl 1);
    1.23 -by (assume_tac 1);
    1.24 -by (Clarify_tac 1);
    1.25 -by (rtac exI 1);
    1.26 -by (rtac conjI 1);
    1.27 -by (rtac refl 1);
    1.28 -by (assume_tac 1);
    1.29 +by (Blast_tac 3);
    1.30 +by (Blast_tac 2);
    1.31 +by (Best_tac 1);
    1.32  qed "steps_union";
    1.33  
    1.34  Goalw [union_def]

     2.1 --- a/src/HOL/WF.ML	Wed Aug 19 10:27:25 1998 +0200
     2.2 +++ b/src/HOL/WF.ML	Wed Aug 19 10:27:49 1998 +0200
     2.3 @@ -176,11 +176,7 @@
     2.4    by (Blast_tac 1);
     2.5   by (blast_tac (claset() addEs [equalityE]) 1);
     2.6  by (Asm_full_simp_tac 1);
     2.7 -by (case_tac "? i. i:I" 1);
     2.8 - by (Clarify_tac 1);
     2.9 - by (EVERY1[dtac bspec, atac, eres_inst_tac[("x","A")]allE]);
    2.10 - by (Blast_tac 1);
    2.11 -by (Blast_tac 1);
    2.12 +by (Fast_tac 1);  (*faster than Blast_tac*)
    2.13  qed "wf_UN";
    2.14  
    2.15  Goalw [Union_def]