# 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;