# HG changeset patch
# User wenzelm
# Date 1191265706 -7200
# Node ID f53f6b08e13a56c5dcf2c608571abffed0511d2a
# Parent  3ab455b3d03b090ede1fa0a730d37c34cffb40ea
misc tuning and update;

diff -r 3ab455b3d03b -r f53f6b08e13a NEWS
--- a/NEWS	Mon Oct 01 21:04:40 2007 +0200
+++ b/NEWS	Mon Oct 01 21:08:26 2007 +0200
@@ -1,8 +1,8 @@
 Isabelle NEWS -- history user-relevant changes
 ==============================================
 
-New in this Isabelle version
-----------------------------
+New in Isabelle2007
+-------------------
 
 *** General ***
 
@@ -1088,23 +1088,6 @@
 is available in HOL/ex/ReflectionEx.thy
 
 
-*** HOL-Algebra ***
-
-* Formalisation of ideals and the quotient construction over rings.
-
-* Order and lattice theory no longer based on records.
-INCOMPATIBILITY.
-
-* Renamed lemmas least_carrier -> least_closed and greatest_carrier ->
-greatest_closed.  INCOMPATIBILITY.
-
-* Method algebra is now set up via an attribute.  For examples see
-Ring.thy.  INCOMPATIBILITY: the method is now weaker on combinations
-of algebraic structures.
-
-* Renamed theory CRing to Ring.
-
-
 *** HOL-Complex ***
 
 * Hyperreal: Functions root and sqrt are now defined on negative real
@@ -1161,6 +1144,30 @@
   (ns)deriv     <-- (ns)cderiv
 
 
+*** HOL-Algebra ***
+
+* Formalisation of ideals and the quotient construction over rings.
+
+* Order and lattice theory no longer based on records.
+INCOMPATIBILITY.
+
+* Renamed lemmas least_carrier -> least_closed and greatest_carrier ->
+greatest_closed.  INCOMPATIBILITY.
+
+* Method algebra is now set up via an attribute.  For examples see
+Ring.thy.  INCOMPATIBILITY: the method is now weaker on combinations
+of algebraic structures.
+
+* Renamed theory CRing to Ring.
+
+
+*** HOL-Nominal ***
+
+* Fully featured support for nominal datatypes (binding structures)
+due to the HOL-Nominal logic.  See HOL/Nominal, HOL/Nominal/Examples,
+and http://isabelle.in.tum.de/nominal/download.html
+
+
 *** ML ***
 
 * ML basics: just one true type int, which coincides with IntInf.int
@@ -1353,7 +1360,7 @@
 operations, notably runtime compilation and evaluation of ML source
 code.
 
-* Support for parall execution, using native multicore support of
+* Support for parallel execution, using native multicore support of
 Poly/ML 5.1.  The theory loader exploits parallelism when processing
 independent theories, according to the given theory header
 specifications. The maximum number of worker threads is specified via