NEWS
changeset 2865 77daca16b2f4
parent 2825 a94dba60d5f2
child 2927 56131a902972
--- 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
-[equalityI];
+* 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;