10 NEWS file distributed with Isabelle for more details. |
10 NEWS file distributed with Isabelle for more details. |
11 |
11 |
12 * Poly/ML 4.0 used by default |
12 * Poly/ML 4.0 used by default |
13 More robust, less disk space required. |
13 More robust, less disk space required. |
14 |
14 |
15 * Pure/Simplifier (Stefan Berghofer) |
15 * Simplifier (Stefan Berghofer) |
16 Proper implementation as a derived rule, outside the kernel! |
16 Proper implementation as a derived rule, outside the kernel! |
|
17 |
|
18 * Improved document preparation (Markus Wenzel) |
|
19 Near math-mode, sub/super scripts, more symbols etc. |
17 |
20 |
18 * Isabelle/Isar (Markus Wenzel) |
21 * Isabelle/Isar (Markus Wenzel) |
19 Numerous usability improvements, e.g. support for initial |
22 Numerous usability improvements, e.g. support for initial |
20 schematic goals, failure prediction of subgoal statements, |
23 schematic goals, failure prediction of subgoal statements, |
21 handling of non-atomic statements in induction. |
24 handling of non-atomic statements in induction. |
22 |
25 |
23 * Improved document preparation (Markus Wenzel) |
|
24 Near math-mode, sub/super scripts, more symbols etc. |
|
25 |
|
26 * HOL/Library (Gertrud Bauer, Tobias Nipkow, Lawrence C Paulson, |
26 * HOL/Library (Gertrud Bauer, Tobias Nipkow, Lawrence C Paulson, |
27 Thomas M Rasmussen, Markus Wenzel) |
27 Thomas M Rasmussen, Markus Wenzel) |
28 A collection of generic theories to be used together with main HOL. |
28 A collection of generic theories to be used together with main HOL. |
29 |
29 |
30 * HOL/Real and HOL/Hyperreal (Jacques Fleuriot and Lawrence C Paulson) |
30 * HOL/Real and HOL/Hyperreal (Jacques Fleuriot, Lawrence C Paulson) |
31 General cleanup, more on nonstandard real analysis. |
31 General cleanup, more on nonstandard real analysis. |
32 |
32 |
33 * HOL/Unix (Markus Wenzel) |
33 * HOL/Unix (Markus Wenzel) |
34 Some Aspects of Unix file-system security; demonstrates |
34 Some Aspects of Unix file-system security; demonstrates |
35 Isabelle/Isar in typical system modelling and verification tasks. |
35 Isabelle/Isar in typical system modelling and verification tasks. |