* 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]
