[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