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

ANNOUNCE

changeset 41604 | 313b0033034a |

parent 37353 | b6222a65bacf |

child 41605 | 7d035da21e9c |

1.1 --- a/ANNOUNCE Mon Jan 17 18:32:16 2011 +0100 1.2 +++ b/ANNOUNCE Mon Jan 17 22:54:08 2011 +0100 1.3 @@ -1,34 +1,34 @@ 1.4 -Subject: Announcing Isabelle2009-2 1.5 +Subject: Announcing Isabelle2011 1.6 To: isabelle-users@cl.cam.ac.uk 1.7 1.8 -Isabelle2009-2 is now available. 1.9 +Isabelle2011 is now available. 1.10 1.11 -This release improves upon Isabelle2009-1 in many respects, see the 1.12 -NEWS file in the distribution for more details. Some notable changes 1.13 -are: 1.14 +This version significantly improves upon Isabelle2009-2, see the NEWS 1.15 +file in the distribution for more details. Some notable changes are: 1.16 1.17 -* Explicit proof terms for type class reasoning. 1.18 +* Experimental Prover IDE based on Isabelle/Scala and jEdit. 1.19 + 1.20 +* Coercive subtyping (configured in HOL/Complex_Main). 1.21 1.22 -* Robust treatment of concrete syntax for different logical entities; 1.23 -mixfix syntax in local proof context. 1.24 +* HOL code generation: Scala as another target language. 1.25 1.26 -* Type declarations and notation within local theory context. 1.27 +* HOL: partial_function definitions. 1.28 1.29 -* HOL: package for quotient types. 1.30 +* HOL: various tool enhancements, including Quickcheck, Nitpick, 1.31 + Sledgehammer, SMT integration. 1.32 1.33 -* HOL code generation: simple concept for abstract datatypes obeying 1.34 -invariants (e.g. red-black trees). 1.35 +* HOL: various additions to theory library, including HOL-Algebra, 1.36 + Imperative_HOL Multivariate_Analysis, Probability. 1.37 1.38 -* HOL: new development of the Reals using Cauchy Sequences. 1.39 - 1.40 -* HOL: reorganization of abstract algebra type class hierarchy. 1.41 +* HOLCF: reorganization of library and related tools. 1.42 1.43 -* HOL: substantial reorganization of main library and related tools. 1.44 +* HOL/SPARK: interactive proof environment for verification conditions 1.45 + generated by the SPARK Ada program verifier. 1.46 1.47 -* HOLCF: reorganization of 'domain' package. 1.48 +* Improved Isabelle/Isar implementation manual (covering Isabelle/ML). 1.49 1.50 1.51 -You may get Isabelle2009-2 from the following mirror sites: 1.52 +You may get Isabelle2011 from the following mirror sites: 1.53 1.54 Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ 1.55 Munich (Germany) http://isabelle.in.tum.de/