--- a/src/HOL/Lex/Automata.ML Wed May 06 13:01:45 1998 +0200
+++ b/src/HOL/Lex/Automata.ML Thu May 07 13:02:23 1998 +0200
@@ -22,12 +22,12 @@
(*** Direct equivalence of NAe and DA ***)
goalw thy [nae2da_def]
- "!Q. (eps A)^* ^^ (DA.delta (nae2da A) w Q) = lift(NAe.delta A w) Q";
+ "!Q. (eps A)^* ^^ (DA.delta (nae2da A) w Q) = steps A w ^^ Q";
by(induct_tac "w" 1);
- by(ALLGOALS Asm_simp_tac);
- by(Blast_tac 1);
+ by (Simp_tac 1);
+by(asm_full_simp_tac (simpset() addsimps [step_def]) 1);
by(Blast_tac 1);
-qed_spec_mp "espclosure_DA_delta_is_lift_NAe_delta";
+qed_spec_mp "espclosure_DA_delta_is_steps";
goalw thy [nae2da_def]
"fin (nae2da A) Q = (? q : (eps A)^* ^^ Q. fin A q)";
@@ -36,8 +36,7 @@
goalw thy [NAe.accepts_def,DA.accepts_def]
"NAe.accepts A w = DA.accepts (nae2da A) w";
-by(simp_tac (simpset() addsimps [lemma,steps_equiv_delta,
- espclosure_DA_delta_is_lift_NAe_delta]) 1);
+by(simp_tac (simpset() addsimps [lemma,espclosure_DA_delta_is_steps]) 1);
by(simp_tac (simpset() addsimps [nae2da_def]) 1);
by(Blast_tac 1);
qed "NAe_DA_equiv";