NEWS

 
 * HOL/ML: even fewer consts are declared as global (see theories Ord,
 Lfp, Gfp, WF); this only affects ML packages that refer to const names
 internally;
 
+* HOL, ZF: syntax for quotienting wrt an equivalence relation changed from
+  A/r to A//r;
+
 * 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

 * fewer consts declared as global (e.g. have to refer to "Lfp.lfp"
 instead of "lfp" internally; affects ML packages only);
 
 * tuned AST representation of nested pairs, avoiding bogus output in
 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;