src/HOL/Lex/RegExp2NA.ML
changeset 5457 367878234bb2
parent 5323 028e00595280
child 5525 896f8234b864
     1.1 --- a/src/HOL/Lex/RegExp2NA.ML	Thu Sep 10 17:27:15 1998 +0200
     1.2 +++ b/src/HOL/Lex/RegExp2NA.ML	Thu Sep 10 17:27:50 1998 +0200
     1.3 @@ -84,17 +84,13 @@
     1.4  Goal
     1.5   "!p. (True#p,q):steps (union L R) w = (? r. q = True # r & (p,r):steps L w)";
     1.6  by (induct_tac "w" 1);
     1.7 -by (ALLGOALS Asm_simp_tac);
     1.8 -(* Blast_tac produces PROOF FAILED for depth 8 *)
     1.9 -by(ALLGOALS Fast_tac);
    1.10 +by Auto_tac;
    1.11  qed_spec_mp "lift_True_over_steps_union";
    1.12  
    1.13  Goal 
    1.14   "!p. (False#p,q):steps (union L R) w = (? r. q = False#r & (p,r):steps R w)";
    1.15  by (induct_tac "w" 1);
    1.16 -by (ALLGOALS Asm_simp_tac);
    1.17 -(* Blast_tac produces PROOF FAILED for depth 8 *)
    1.18 -by(ALLGOALS Fast_tac);
    1.19 +by Auto_tac;
    1.20  qed_spec_mp "lift_False_over_steps_union";
    1.21  
    1.22  AddIffs [lift_True_over_steps_union,lift_False_over_steps_union];
    1.23 @@ -181,11 +177,7 @@
    1.24  Goal
    1.25   "!p. (False#p,q): steps (conc L R) w = (? r. q=False#r & (p,r): steps R w)";
    1.26  by (induct_tac "w" 1);
    1.27 - by (Simp_tac 1);
    1.28 - by(Fast_tac 1);
    1.29 -by (Simp_tac 1);
    1.30 -(* Blast_tac produces PROOF FAILED for depth 8 *)
    1.31 -by(Fast_tac 1);
    1.32 +by Auto_tac;
    1.33  qed_spec_mp "False_steps_conc";
    1.34  AddIffs [False_steps_conc];
    1.35