# HG changeset patch
# User wenzelm
# Date 1230063506 -3600
# Node ID 9903e84a9c9c2bbcbd8c75568998a0c7be507f1a
# Parent  86e9f91a0ba4b99ca59224271f61829329726494
* Proofs of are run in parallel on multi-core systems;
* High-level support for concurrent ML programming;

diff -r 86e9f91a0ba4 -r 9903e84a9c9c NEWS
--- a/NEWS	Tue Dec 23 21:03:47 2008 +0100
+++ b/NEWS	Tue Dec 23 21:18:26 2008 +0100
@@ -42,6 +42,11 @@
 ISABELLE_HOME_USER can be changed in Isabelle/etc/settings of any
 Isabelle distribution.
 
+* Proofs of fully specified statements are run in parallel on
+multi-core systems.  A speedup factor of 2-3 can be expected on a
+regular 4-core machine, if the initial heap space is made reasonably
+large (cf. Poly/ML option -H).
+
 * The Isabelle System Manual (system) has been updated, with formally
 checked references as hyperlinks.
 
@@ -55,8 +60,8 @@
 * Removed exotic 'token_translation' command.  INCOMPATIBILITY, use ML
 interface instead.
 
-* There is a new lexical item "float" with syntax ["-"] digit+ "." digit+,
-without spaces.
+* There is a new syntactic category "float_const" for signed decimal
+fractions (e.g. 123.45 or -123.45).
 
 
 *** Pure ***
@@ -391,6 +396,13 @@
 
 *** ML ***
 
+* High-level support for concurrent ML programming, see
+src/Pure/Cuncurrent.  The data-oriented model of "future values" is
+particularly convenient to organize independent functional
+computations.  The concept of "synchronized variables" provides a
+higher-order interface for components with shared state, avoiding the
+delicate details of internal mutexes and condition variables.
+
 * Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm
 to 'a -> thm, while results are always tagged with an authentic oracle
 name.  The Isar command 'oracle' is now polymorphic, no argument type
@@ -860,8 +872,8 @@
 print_mode_active, PrintMode.setmp etc.  INCOMPATIBILITY.
 
 * Functions system/system_out provide a robust way to invoke external
-shell commands, with propagation of interrupts (requires Poly/ML 5.2).
-Do not use OS.Process.system etc. from the basis library!
+shell commands, with propagation of interrupts (requires Poly/ML
+5.2.1).  Do not use OS.Process.system etc. from the basis library!
 
 
 *** System ***