removed duplicate proof and small mod.
--- a/src/HOL/Lex/RegExp.thy Mon Jun 25 15:36:55 2001 +0200
+++ b/src/HOL/Lex/RegExp.thy Tue Jun 26 15:28:49 2001 +0200
@@ -16,10 +16,10 @@
consts lang :: 'a rexp => 'a list set
primrec
-lang_Emp "lang Empty = {}"
-lang_Atom "lang (Atom a) = {[a]}"
-lang_Un "lang (Union el er) = (lang el) Un (lang er)"
-lang_Conc "lang (Conc el er) = RegSet.conc (lang el) (lang er)"
-lang_Star "lang (Star e) = RegSet.star(lang e)"
+"lang Empty = {}"
+"lang (Atom a) = {[a]}"
+"lang (Union el er) = (lang el) Un (lang er)"
+"lang (Conc el er) = RegSet.conc (lang el) (lang er)"
+"lang (Star e) = RegSet.star(lang e)"
end
--- a/src/HOL/Lex/RegExp2NA.ML Mon Jun 25 15:36:55 2001 +0200
+++ b/src/HOL/Lex/RegExp2NA.ML Tue Jun 26 15:28:49 2001 +0200
@@ -346,31 +346,6 @@
Goal
"!r. (start A,r) : steps (plus A) w --> \
\ (? us v. w = concat us @ v & \
-\ (!u:set us. u ~= [] & accepts A u) & \
-\ (start A,r) : steps A v)";
-by (rev_induct_tac "w" 1);
- by (Simp_tac 1);
- by (res_inst_tac [("x","[]")] exI 1);
- by (Simp_tac 1);
-by (Simp_tac 1);
-by (Clarify_tac 1);
-by (etac allE 1 THEN mp_tac 1);
-by (Clarify_tac 1);
-by (etac disjE 1);
- by (res_inst_tac [("x","us")] exI 1);
- by (Asm_simp_tac 1);
- by (Blast_tac 1);
-by (case_tac "v" 1);
- by (res_inst_tac [("x","us")] exI 1);
- by (Asm_full_simp_tac 1);
-by (res_inst_tac [("x","us@[v]")] exI 1);
-by (asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
-by (Blast_tac 1);
-qed_spec_mp "start_steps_plusD";
-
-Goal
- "!r. (start A,r) : steps (plus A) w --> \
-\ (? us v. w = concat us @ v & \
\ (!u:set us. accepts A u) & \
\ (start A,r) : steps A v)";
by (rev_induct_tac "w" 1);