--- 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]