# HG changeset patch
# User paulson
# Date 859986877 -7200
# Node ID 77daca16b2f462c53e28052f915bec814bdb41bc
# Parent  103bd2dc33b03dc9d0b5a3331cea8646d1f9dce1
ZF.thy is again usable

diff -r 103bd2dc33b0 -r 77daca16b2f4 NEWS
--- 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;