src/HOL/Lex/RegExp2NAe.ML
changeset 14401 477380c74c1d
parent 13145 59bc43b51aa2
child 14428 bb2b0e10d9be
     1.1 --- a/src/HOL/Lex/RegExp2NAe.ML	Thu Feb 19 17:57:54 2004 +0100
     1.2 +++ b/src/HOL/Lex/RegExp2NAe.ML	Thu Feb 19 18:24:08 2004 +0100
     1.3 @@ -408,7 +408,7 @@
     1.4  
     1.5  Goalw [conc_def]
     1.6   "!L R. fin(conc L R) p = (? 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  qed_spec_mp "final_conc";
    1.10  
    1.11  Goal