| changeset 5265 | 9d1d4c43c76d |
| parent 5241 | e5129172cb2b |
| child 5268 | 59ef39008514 |
--- a/src/ZF/AC/WO6_WO1.ML Thu Aug 06 10:37:39 1998 +0200 +++ b/src/ZF/AC/WO6_WO1.ML Thu Aug 06 10:38:57 1998 +0200 @@ -375,7 +375,7 @@ (* ********************************************************************** *) Goalw [WO6_def, NN_def] "!!y. WO6 ==> NN(y) ~= 0"; -by (fast_tac (ZF_cs addEs [equals0E]) 1); +by (fast_tac ZF_cs 1); (*SLOW if current claset is used*) qed "WO6_imp_NN_not_empty"; (* ********************************************************************** *)