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 Jun 07 11:42:42 2010 +0200 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 -* Robust treatment of concrete syntax for different logical entities; 1.21 -mixfix syntax in local proof context. 1.22 +* Coercive subtyping (configured in HOL/Complex_Main). 1.23 1.24 -* Type declarations and notation within local theory context. 1.25 +* HOL code generation: Scala as another target language. 1.26 1.27 -* HOL: package for quotient types. 1.28 +* HOL: partial_function definitions. 1.29 1.30 -* HOL code generation: simple concept for abstract datatypes obeying 1.31 -invariants (e.g. red-black trees). 1.32 +* HOL: various tool enhancements, including Quickcheck, Nitpick, 1.33 + Sledgehammer, SMT integration. 1.34 1.35 -* HOL: new development of the Reals using Cauchy Sequences. 1.36 +* HOL: various additions to theory library, including HOL-Algebra, 1.37 + Imperative_HOL Multivariate_Analysis, Probability. 1.38 1.39 -* HOL: reorganization of abstract algebra type class hierarchy. 1.40 +* HOLCF: reorganization of library and related tools. 1.41 1.42 -* HOL: substantial reorganization of main library and related tools. 1.43 +* HOL/SPARK: interactive proof environment for verification conditions 1.44 + generated by the SPARK Ada program verifier. 1.45 1.46 -* HOLCF: reorganization of 'domain' package. 1.47 +* Improved Isabelle/Isar implementation manual (covering Isabelle/ML). 1.48 1.49 1.50 -You may get Isabelle2009-2 from the following mirror sites: 1.51 +You may get Isabelle2011 from the following mirror sites: 1.52 1.53 Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ 1.54 Munich (Germany) http://isabelle.in.tum.de/