src/ZF/Resid/Residuals.ML

 (*     Residuals are comp and regular                                        *)
 (* ------------------------------------------------------------------------- *)
 
 Goal "u~v ==> ALL w. u~w --> v~w --> regular(w) --> (u|>w) ~ (v|>w)";
 by (etac Scomp.induct 1);
-by Auto_tac;
+by (ALLGOALS Force_tac);
 qed_spec_mp "residuals_preserve_comp";
 
 
 Goal "u~v ==> regular(u) --> regular(v) --> regular(u|>v)";
 by (etac Scomp.induct 1);