ANNOUNCE
author bulwahn
Mon Nov 23 21:56:07 2009 +0100 (2009-11-23)
changeset 33871 caab5399bb2d
parent 33866 34e45b2afe43
child 33873 e9120a7b2779
permissions -rw-r--r--
merged
wenzelm@33842
     1
Subject: Announcing Isabelle2009-1
wenzelm@9928
     2
To: isabelle-users@cl.cam.ac.uk
wenzelm@9928
     3
wenzelm@33842
     4
Isabelle2009-1 is now available.
wenzelm@17544
     5
wenzelm@33842
     6
This release improves upon Isabelle2009 in many ways, see the NEWS
wenzelm@30848
     7
file in the distribution for more details.  Some important changes
wenzelm@30848
     8
are:
wenzelm@27007
     9
haftmann@33866
    10
* Proof method "smt" for a combination of first-order logic with equality,
haftmann@33866
    11
linear and nonlinear (natural/integer/real) arithmetic, and fixed-size bitvectors.
haftmann@33866
    12
haftmann@33866
    13
* Counterexample generator tool »nitpick« based on the Kodkod relational model finder.
haftmann@33866
    14
haftmann@33866
    15
* Predicate compiler turning inductive into (executable) equational specifications.
haftmann@33866
    16
haftmann@33866
    17
* Refined number theory.
wenzelm@30890
    18
haftmann@33866
    19
* Various parts of multivariate analysis.
haftmann@33866
    20
haftmann@33866
    21
* HOL-Boogie: an interactive prover back-end for Boogie and VCC.
haftmann@33866
    22
haftmann@33866
    23
* Revised tutorial on locales.
haftmann@33866
    24
haftmann@33866
    25
* New definitional domain package for HOLCF.
haftmann@33866
    26
haftmann@33866
    27
* Support for Poly/ML 5.3.0, with improved reporting of compiler errors and run-time exceptions, including detailed source positions.
wenzelm@12983
    28
wenzelm@33842
    29
You may get Isabelle2009-1 from the following mirror sites:
wenzelm@9928
    30
haftmann@27085
    31
  Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
haftmann@17696
    32
  Munich (Germany)     http://isabelle.in.tum.de/
kleing@14616
    33
  Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/