NEWS

 rather than just a warning (in interactive mode);
 
 
 *** HOL ***
 
-* GroupTheory: new, experimental summation operator for abelian groups.
-
 * New tactic "trans_tac" and method "trans" instantiate
 Provers/linorder.ML for axclasses "order" and "linorder" (predicates
 "<=", "<" and "="). 
 
 * function INCOMPATIBILITIES: Pi-sets have been redefined and moved from main 

 are distributed over a sum of terms;
 
 * induct over a !!-quantified statement (say !!x1..xn):
   each "case" automatically performs "fix x1 .. xn" with exactly those names.
 
-* GroupTheory: converted to Isar theories, using locales with implicit structures;
-
 * Real/HahnBanach: updated and adapted to locales;
+
+* GroupTheory: converted to Isar theories, using locales with implicit
+structures.  Also a new, experimental summation operator for abelian groups;
+
+* NumberTheory: added Gauss's law of quadratic reciprocity (by Avigad, Gray and
+Kramer);
+
+* UNITY: added the Meier-Sanders theory of progress sets;
 
 
 *** ZF ***
 
 * ZF/Constructible: consistency proof for AC (Gödel's constructible
 universe, etc.);
 
-* Main ZF: many theories converted to new-style format;
+* Main ZF: virtually all theories converted to new-style format;
 
 
 *** ML ***
 
 * Pure: Tactic.prove provides sane interface for internal proofs;