[isabelle-dev] NEWS

Makarius makarius at sketis.net
Tue Dec 23 21:24:24 CET 2008


* 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).  [Poly/ML 5.2.1 or later]

* 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 mutexes and condition variables.  [Poly/ML 5.2.1 or later]



More information about the isabelle-dev mailing list