--- a/src/HOL/Lex/RegExp2NA.ML Fri Oct 23 20:36:21 1998 +0200
+++ b/src/HOL/Lex/RegExp2NA.ML Fri Oct 23 20:44:34 1998 +0200
@@ -84,13 +84,13 @@
Goal
"!p. (True#p,q):steps (union L R) w = (? r. q = True # r & (p,r):steps L w)";
by (induct_tac "w" 1);
-by Auto_tac;
+by (ALLGOALS Force_tac);
qed_spec_mp "lift_True_over_steps_union";
Goal
"!p. (False#p,q):steps (union L R) w = (? r. q = False#r & (p,r):steps R w)";
by (induct_tac "w" 1);
-by Auto_tac;
+by (ALLGOALS Force_tac);
qed_spec_mp "lift_False_over_steps_union";
AddIffs [lift_True_over_steps_union,lift_False_over_steps_union];
@@ -177,7 +177,7 @@
Goal
"!p. (False#p,q): steps (conc L R) w = (? r. q=False#r & (p,r): steps R w)";
by (induct_tac "w" 1);
-by Auto_tac;
+by (ALLGOALS Force_tac);
qed_spec_mp "False_steps_conc";
AddIffs [False_steps_conc];