summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

ANNOUNCE

changeset 13042 | d8a345d9e067 |

parent 13010 | 3437d8d89803 |

child 13045 | 1db0bdda1d32 |

1.1 --- a/ANNOUNCE Thu Mar 07 22:52:07 2002 +0100 1.2 +++ b/ANNOUNCE Thu Mar 07 23:21:19 2002 +0100 1.3 @@ -18,7 +18,7 @@ 1.4 Isabelle2002 is the official version to go along with that book 1.5 (by Tobias Nipkow, Larry Paulson, Markus Wenzel). 1.6 1.7 - * Pure: explicit proof terms for all internal inferences: 1.8 + * Pure: explicit proof terms for all internal inferences; 1.9 object-logics, proof tools etc. will benefit automatically 1.10 (by Stefan Berghofer). 1.11 1.12 @@ -27,28 +27,30 @@ 1.13 operations, and type-inference for structured specifications 1.14 (by Markus Wenzel). 1.15 1.16 - * Pure/Isar: streamlined induction proof patterns 1.17 + * Pure/Isar: streamlined cases/induction proof patterns 1.18 (by Markus Wenzel). 1.19 1.20 * Pure/HOL: infrastructure for generating functional and relational 1.21 - code, using the ML run-time environment (by Stefan Berghofer). 1.22 + code, using the ML run-time environment 1.23 + (by Stefan Berghofer). 1.24 1.25 - * HOL/library: numerals on all number types; several 1.26 - improvements of tuple and record types; new definite description 1.27 - operator; keep Hilbert's epsilon (Axiom of Choice) out of basic theories. 1.28 + * HOL/library: numerals on all number types; several improvements of 1.29 + tuple and record types; new definite description operator; keep 1.30 + Hilbert's epsilon (Axiom of Choice) out of basic theories 1.31 + (by Stefan Berghofer, Larry Paulson, Markus Wenzel). 1.32 1.33 * HOL/Bali: large application concerning formal treatment of Java. 1.34 (by David von Oheimb and Norbert Schirmer). 1.35 1.36 * HOL/HoareParallel: large application concerning verification of 1.37 parallel imperative programs (Owicki-Gries method, Rely-Guarantee 1.38 - method, examples of garbage collection, mutual exclusion, etc.) 1.39 + method, examples of garbage collection, mutual exclusion) 1.40 (by Leonor Prensa Nieto). 1.41 1.42 * HOL/GroupTheory: group theory examples including Sylow's theorem 1.43 - (by Florian Kammüller). 1.44 + (by Florian Kammueller). 1.45 1.46 - * HOL/IMP: new proofs in Isar format 1.47 + * HOL/IMP: several new proofs in Isar format 1.48 (by Gerwin Klein). 1.49 1.50 * HOL/MicroJava: exception handling on the bytecode level 1.51 @@ -61,10 +63,8 @@ 1.52 (by Markus Wenzel). 1.53 1.54 * System: support for Poly/ML 4.1.1 and PolyML/4.1.2, admitting 1.55 - larger heap size of applications. 1.56 - 1.57 - * System: support for MacOS X (for Poly/ML and SML/NJ). 1.58 - 1.59 + larger heap size of applications; support for MacOS X (Poly/ML and 1.60 + SML/NJ). 1.61 1.62 You may get Isabelle2002 from any of the following mirror sites: 1.63