equal
deleted
inserted
replaced
43 Isabelle distribution. |
43 Isabelle distribution. |
44 |
44 |
45 * Proofs of fully specified statements are run in parallel on |
45 * Proofs of fully specified statements are run in parallel on |
46 multi-core systems. A speedup factor of 2-3 can be expected on a |
46 multi-core systems. A speedup factor of 2-3 can be expected on a |
47 regular 4-core machine, if the initial heap space is made reasonably |
47 regular 4-core machine, if the initial heap space is made reasonably |
48 large (cf. Poly/ML option -H). |
48 large (cf. Poly/ML option -H). [Poly/ML 5.2.1 or later] |
49 |
49 |
50 * The Isabelle System Manual (system) has been updated, with formally |
50 * The Isabelle System Manual (system) has been updated, with formally |
51 checked references as hyperlinks. |
51 checked references as hyperlinks. |
52 |
52 |
53 * Generalized Isar history, with support for linear undo, direct state |
53 * Generalized Isar history, with support for linear undo, direct state |
399 * High-level support for concurrent ML programming, see |
399 * High-level support for concurrent ML programming, see |
400 src/Pure/Cuncurrent. The data-oriented model of "future values" is |
400 src/Pure/Cuncurrent. The data-oriented model of "future values" is |
401 particularly convenient to organize independent functional |
401 particularly convenient to organize independent functional |
402 computations. The concept of "synchronized variables" provides a |
402 computations. The concept of "synchronized variables" provides a |
403 higher-order interface for components with shared state, avoiding the |
403 higher-order interface for components with shared state, avoiding the |
404 delicate details of internal mutexes and condition variables. |
404 delicate details of mutexes and condition variables. [Poly/ML 5.2.1 |
|
405 or later] |
405 |
406 |
406 * Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm |
407 * Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm |
407 to 'a -> thm, while results are always tagged with an authentic oracle |
408 to 'a -> thm, while results are always tagged with an authentic oracle |
408 name. The Isar command 'oracle' is now polymorphic, no argument type |
409 name. The Isar command 'oracle' is now polymorphic, no argument type |
409 is specified. INCOMPATIBILITY, need to simplify existing oracle code |
410 is specified. INCOMPATIBILITY, need to simplify existing oracle code |