src/HOL/Lex/RegExp2NA.ML
changeset 12487 bbd564190c9b
parent 11379 0c90ffd3f3e2
child 12792 b344226f924c
     1.1 --- a/src/HOL/Lex/RegExp2NA.ML	Thu Dec 13 15:45:03 2001 +0100
     1.2 +++ b/src/HOL/Lex/RegExp2NA.ML	Thu Dec 13 16:47:35 2001 +0100
     1.3 @@ -26,7 +26,7 @@
     1.4   "([False],[False]) : steps (atom a) w = (w = [])";
     1.5  by (induct_tac "w" 1);
     1.6   by (Simp_tac 1);
     1.7 -by (asm_simp_tac (simpset() addsimps [comp_def]) 1);
     1.8 +by (asm_simp_tac (simpset() addsimps [rel_comp_def]) 1);
     1.9  qed "False_False_in_steps_atom";
    1.10  
    1.11  Goal
    1.12 @@ -34,7 +34,7 @@
    1.13  by (induct_tac "w" 1);
    1.14   by (asm_simp_tac (simpset() addsimps [start_atom]) 1);
    1.15  by (asm_full_simp_tac (simpset()
    1.16 -     addsimps [False_False_in_steps_atom,comp_def,start_atom]) 1);
    1.17 +     addsimps [False_False_in_steps_atom,rel_comp_def,start_atom]) 1);
    1.18  qed "start_fin_in_steps_atom";
    1.19  
    1.20  Goal