# HG changeset patch
# User nipkow
# Date 993562129 -7200
# Node ID 0c90ffd3f3e29c7b9ef1df02ca115c9db7dd4496
# Parent  5c84a5ca3a21473166e59937488e44e65a42ba3d
removed duplicate proof and small mod.

diff -r 5c84a5ca3a21 -r 0c90ffd3f3e2 src/HOL/Lex/RegExp.thy
--- 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
diff -r 5c84a5ca3a21 -r 0c90ffd3f3e2 src/HOL/Lex/RegExp2NA.ML
--- 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);