src/HOL/Lex/RegExp2NA.ML
changeset 14401 477380c74c1d
parent 13145 59bc43b51aa2
child 14428 bb2b0e10d9be
     1.1 --- a/src/HOL/Lex/RegExp2NA.ML	Thu Feb 19 17:57:54 2004 +0100
     1.2 +++ b/src/HOL/Lex/RegExp2NA.ML	Thu Feb 19 18:24:08 2004 +0100
     1.3 @@ -249,7 +249,7 @@
     1.4  Goalw [conc_def]
     1.5   "!L R. fin(conc L R) p = ((fin R (start R) & (? s. p = True#s & fin L s)) | \
     1.6  \                          (? s. p = False#s & fin R s))";
     1.7 -by (simp_tac (simpset() addsplits [list.split]) 1);
     1.8 +by (simp_tac (simpset() addsplits [thm"list.split"]) 1);
     1.9  by (Blast_tac 1);
    1.10  qed_spec_mp "final_conc";
    1.11