misc tuning and update;
authorwenzelm
Mon Oct 01 21:08:26 2007 +0200 (2007-10-01)
changeset 24801f53f6b08e13a
parent 24800 3ab455b3d03b
child 24802 6bd8ec8f3fc8
misc tuning and update;
NEWS
     1.1 --- a/NEWS	Mon Oct 01 21:04:40 2007 +0200
     1.2 +++ b/NEWS	Mon Oct 01 21:08:26 2007 +0200
     1.3 @@ -1,8 +1,8 @@
     1.4  Isabelle NEWS -- history user-relevant changes
     1.5  ==============================================
     1.6  
     1.7 -New in this Isabelle version
     1.8 -----------------------------
     1.9 +New in Isabelle2007
    1.10 +-------------------
    1.11  
    1.12  *** General ***
    1.13  
    1.14 @@ -1088,23 +1088,6 @@
    1.15  is available in HOL/ex/ReflectionEx.thy
    1.16  
    1.17  
    1.18 -*** HOL-Algebra ***
    1.19 -
    1.20 -* Formalisation of ideals and the quotient construction over rings.
    1.21 -
    1.22 -* Order and lattice theory no longer based on records.
    1.23 -INCOMPATIBILITY.
    1.24 -
    1.25 -* Renamed lemmas least_carrier -> least_closed and greatest_carrier ->
    1.26 -greatest_closed.  INCOMPATIBILITY.
    1.27 -
    1.28 -* Method algebra is now set up via an attribute.  For examples see
    1.29 -Ring.thy.  INCOMPATIBILITY: the method is now weaker on combinations
    1.30 -of algebraic structures.
    1.31 -
    1.32 -* Renamed theory CRing to Ring.
    1.33 -
    1.34 -
    1.35  *** HOL-Complex ***
    1.36  
    1.37  * Hyperreal: Functions root and sqrt are now defined on negative real
    1.38 @@ -1161,6 +1144,30 @@
    1.39    (ns)deriv     <-- (ns)cderiv
    1.40  
    1.41  
    1.42 +*** HOL-Algebra ***
    1.43 +
    1.44 +* Formalisation of ideals and the quotient construction over rings.
    1.45 +
    1.46 +* Order and lattice theory no longer based on records.
    1.47 +INCOMPATIBILITY.
    1.48 +
    1.49 +* Renamed lemmas least_carrier -> least_closed and greatest_carrier ->
    1.50 +greatest_closed.  INCOMPATIBILITY.
    1.51 +
    1.52 +* Method algebra is now set up via an attribute.  For examples see
    1.53 +Ring.thy.  INCOMPATIBILITY: the method is now weaker on combinations
    1.54 +of algebraic structures.
    1.55 +
    1.56 +* Renamed theory CRing to Ring.
    1.57 +
    1.58 +
    1.59 +*** HOL-Nominal ***
    1.60 +
    1.61 +* Fully featured support for nominal datatypes (binding structures)
    1.62 +due to the HOL-Nominal logic.  See HOL/Nominal, HOL/Nominal/Examples,
    1.63 +and http://isabelle.in.tum.de/nominal/download.html
    1.64 +
    1.65 +
    1.66  *** ML ***
    1.67  
    1.68  * ML basics: just one true type int, which coincides with IntInf.int
    1.69 @@ -1353,7 +1360,7 @@
    1.70  operations, notably runtime compilation and evaluation of ML source
    1.71  code.
    1.72  
    1.73 -* Support for parall execution, using native multicore support of
    1.74 +* Support for parallel execution, using native multicore support of
    1.75  Poly/ML 5.1.  The theory loader exploits parallelism when processing
    1.76  independent theories, according to the given theory header
    1.77  specifications. The maximum number of worker threads is specified via