# HG changeset patch
# User paulson
# Date 963996950 -7200
# Node ID 0b039a3575eb38b7633218b74708222b223475af
# Parent  3bab31b55a951f32403e20d38fcc4885ada28579
// change; also moved entry for AddIffs

diff -r 3bab31b55a95 -r 0b039a3575eb NEWS
--- a/NEWS	Tue Jul 18 21:44:42 2000 +0200
+++ b/NEWS	Wed Jul 19 10:55:50 2000 +0200
@@ -41,10 +41,10 @@
 Lfp, Gfp, WF); this only affects ML packages that refer to const names
 internally;
 
-* Isar: changed syntax of local blocks from {{ }} to { };
+* HOL, ZF: syntax for quotienting wrt an equivalence relation changed from
+  A/r to A//r;
 
-* FOL, ZF: AddIffs now available, giving theorems of the form P<->Q to the
-  simplifier and classical reasoner simultaneously;
+* Isar: changed syntax of local blocks from {{ }} to { };
 
 * Provers: Blast_tac now warns of and ignores "weak elimination rules" e.g.
   [| inj ?f;          ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W
@@ -239,6 +239,12 @@
 case of overlap with user translations (e.g. judgements over tuples);
 
 
+*** FOL & ZF ***
+
+* AddIffs now available, giving theorems of the form P<->Q to the
+  simplifier and classical reasoner simultaneously;
+
+
 *** General ***
 
 * AST translation rules no longer require constant head on LHS;