summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

ANNOUNCE

changeset 13042 | d8a345d9e067 |

parent 13010 | 3437d8d89803 |

child 13045 | 1db0bdda1d32 |

--- a/ANNOUNCE Thu Mar 07 22:52:07 2002 +0100 +++ b/ANNOUNCE Thu Mar 07 23:21:19 2002 +0100 @@ -18,7 +18,7 @@ Isabelle2002 is the official version to go along with that book (by Tobias Nipkow, Larry Paulson, Markus Wenzel). - * Pure: explicit proof terms for all internal inferences: + * Pure: explicit proof terms for all internal inferences; object-logics, proof tools etc. will benefit automatically (by Stefan Berghofer). @@ -27,28 +27,30 @@ operations, and type-inference for structured specifications (by Markus Wenzel). - * Pure/Isar: streamlined induction proof patterns + * Pure/Isar: streamlined cases/induction proof patterns (by Markus Wenzel). * Pure/HOL: infrastructure for generating functional and relational - code, using the ML run-time environment (by Stefan Berghofer). + code, using the ML run-time environment + (by Stefan Berghofer). - * HOL/library: numerals on all number types; several - improvements of tuple and record types; new definite description - operator; keep Hilbert's epsilon (Axiom of Choice) out of basic theories. + * HOL/library: numerals on all number types; several improvements of + tuple and record types; new definite description operator; keep + Hilbert's epsilon (Axiom of Choice) out of basic theories + (by Stefan Berghofer, Larry Paulson, Markus Wenzel). * HOL/Bali: large application concerning formal treatment of Java. (by David von Oheimb and Norbert Schirmer). * HOL/HoareParallel: large application concerning verification of parallel imperative programs (Owicki-Gries method, Rely-Guarantee - method, examples of garbage collection, mutual exclusion, etc.) + method, examples of garbage collection, mutual exclusion) (by Leonor Prensa Nieto). * HOL/GroupTheory: group theory examples including Sylow's theorem - (by Florian Kammüller). + (by Florian Kammueller). - * HOL/IMP: new proofs in Isar format + * HOL/IMP: several new proofs in Isar format (by Gerwin Klein). * HOL/MicroJava: exception handling on the bytecode level @@ -61,10 +63,8 @@ (by Markus Wenzel). * System: support for Poly/ML 4.1.1 and PolyML/4.1.2, admitting - larger heap size of applications. - - * System: support for MacOS X (for Poly/ML and SML/NJ). - + larger heap size of applications; support for MacOS X (Poly/ML and + SML/NJ). You may get Isabelle2002 from any of the following mirror sites: