# HG changeset patch
# User paulson
# Date 903515269 -7200
# Node ID 2f7d09a927c467fc0df4deceee22700d03cac118
# Parent  721bf1a13f1a5ca4aa24a3ef6e9221d1bea60e9a
tidied

diff -r 721bf1a13f1a -r 2f7d09a927c4 src/HOL/Lex/RegExp2NAe.ML
--- 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]
diff -r 721bf1a13f1a -r 2f7d09a927c4 src/HOL/WF.ML
--- 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]