tidied
authorpaulson
Mon, 01 Mar 1999 18:37:52 +0100
changeset 6294 bc084e1b4d8d
parent 6293 2a4357301973
child 6295 351b3c2b0d83
tidied
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]