# HG changeset patch
# User paulson
# Date 963578795 -7200
# Node ID 5d9f02e7556900519288ca896edfe9f39728122d
# Parent  f0c2b71db81bf57b50a2de77dceba97864f46b1b
AddIffs

diff -r f0c2b71db81b -r 5d9f02e75569 NEWS
--- a/NEWS	Fri Jul 14 13:57:00 2000 +0200
+++ b/NEWS	Fri Jul 14 14:46:35 2000 +0200
@@ -41,12 +41,15 @@
 
 * Isar: changed syntax of local blocks from {{ }} to { };
 
+* FOL, ZF: AddIffs now available, giving theorems of the form P<->Q to the
+  simplifier and classical reasoner simultaneously;
+
 * Provers: Blast_tac now warns of and ignores "weak elimination rules" e.g.
   [| inj ?f;          ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W
 use instead the strong form,
   [| inj ?f; ~ ?W ==> ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W
 In HOL, FOL and ZF the function cla_make_elim will create such rules
-from destruct-rules.
+from destruct-rules;
 
 * ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global
 timing flag supersedes proof_timing and Toplevel.trace;