src/HOL/Lex/RegExp2NA.ML
changeset 13145 59bc43b51aa2
parent 12792 b344226f924c
child 14401 477380c74c1d
     1.1 --- a/src/HOL/Lex/RegExp2NA.ML	Mon May 13 13:22:15 2002 +0200
     1.2 +++ b/src/HOL/Lex/RegExp2NA.ML	Mon May 13 15:27:28 2002 +0200
     1.3 @@ -348,7 +348,7 @@
     1.4  \     (? us v. w = concat us @ v & \
     1.5  \              (!u:set us. accepts A u) & \
     1.6  \              (start A,r) : steps A v)";
     1.7 -by (rev_induct_tac "w" 1);
     1.8 +by (res_inst_tac [("xs","w")] rev_induct 1);
     1.9   by (Simp_tac 1);
    1.10   by (res_inst_tac [("x","[]")] exI 1);
    1.11   by (Simp_tac 1);
    1.12 @@ -368,7 +368,7 @@
    1.13  Goal
    1.14   "us ~= [] --> (!u : set us. accepts A u) --> accepts (plus A) (concat us)";
    1.15  by (simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
    1.16 -by (rev_induct_tac "us" 1);
    1.17 +by (res_inst_tac [("xs","us")] rev_induct 1);
    1.18   by (Simp_tac 1);
    1.19  by (rename_tac "u us" 1);
    1.20  by (Simp_tac 1);