tidied

--- a/src/HOL/Lex/RegExp2NAe.ML	Wed Aug 19 10:27:25 1998 +0200
+++ b/src/HOL/Lex/RegExp2NAe.ML	Wed Aug 19 10:27:49 1998 +0200
@@ -211,28 +211,9 @@
 by (Clarify_tac 1);
 by (rtac compI 1);
 by (rtac compI 1);
-by (rtac (epsclosure_start_step_union RS iffD2) 1);
-by (rtac disjI2 1);
-by (rtac exI 1);
-by (rtac conjI 1);
-by (rtac (start_eps_union RS iffD2) 1);
-by (rtac disjI2 1);
-by (rtac refl 1);
-by (Clarify_tac 1);
-by (rtac exI 1);
-by (rtac conjI 1);
-by (rtac refl 1);
-by (assume_tac 1);
-by (Clarify_tac 1);
-by (rtac exI 1);
-by (rtac conjI 1);
-by (rtac refl 1);
-by (assume_tac 1);
-by (Clarify_tac 1);
-by (rtac exI 1);
-by (rtac conjI 1);
-by (rtac refl 1);
-by (assume_tac 1);
+by (Blast_tac 3);
+by (Blast_tac 2);
+by (Best_tac 1);
 qed "steps_union";
 
 Goalw [union_def]

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