# HG changeset patch
# User paulson
# Date 920309872 -3600
# Node ID bc084e1b4d8dd8e0b4641889c2c00d4fcc6b53e4
# Parent  2a435730197388d652fa2488aaeede73f025c304
tidied

diff -r 2a4357301973 -r bc084e1b4d8d src/HOL/Lex/Automata.ML
--- a/src/HOL/Lex/Automata.ML	Mon Mar 01 18:37:23 1999 +0100
+++ b/src/HOL/Lex/Automata.ML	Mon Mar 01 18:37:52 1999 +0100
@@ -9,8 +9,7 @@
 Goalw [na2da_def]
  "!Q. DA.delta (na2da A) w Q = Union(NA.delta A w `` Q)";
 by (induct_tac "w" 1);
- by (ALLGOALS Asm_simp_tac);
- by (ALLGOALS Blast_tac);
+ by Auto_tac;
 qed_spec_mp "DA_delta_is_lift_NA_delta";
 
 Goalw [DA.accepts_def,NA.accepts_def]