ZF.thy is again usable
Wed, 02 Apr 1997 15:14:37 +0200
changeset 2865 77daca16b2f4
parent 2864 103bd2dc33b0
child 2866 0a648ebbf6d4
ZF.thy is again usable
--- a/NEWS	Wed Apr 02 11:59:02 1997 +0200
+++ b/NEWS	Wed Apr 02 15:14:37 1997 +0200
@@ -75,10 +75,9 @@
 * HOL/ex/Ring.thy declares cring_simp, which solves equational
 problems in commutative rings, using axiomatic type classes for + and *;
-* ZF now has Fast_tac, Simp_tac and Auto_tac.  WARNING: don't use
-ZF.thy anymore!  Contains fewer defs and could make a bogus simpset.
-Beware of Union_iff.  eq_cs is gone, can be put back as ZF_cs addSIs
+* ZF now has Fast_tac, Simp_tac and Auto_tac.  Union_iff is a now a default
+rewrite rule; this may affect some proofs.  eq_cs is gone but can be put back
+as ZF_cs addSIs [equalityI];
 * more examples in HOL/MiniML and HOL/Auth;