ANNOUNCE
author haftmann
Tue Nov 24 12:29:08 2009 +0100 (2009-11-24)
changeset 33881 d8958955ecb5
parent 33873 e9120a7b2779
child 33914 d17f447fec02
permissions -rw-r--r--
consisten upper/lower case
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
wenzelm@33873
    10
* Isabelle tool "wwwfind" provides web interface for 'find_theorems'
wenzelm@33873
    11
on a given logic image.
haftmann@33866
    12
wenzelm@33873
    13
* HOL-SMT: proof method "smt" for a combination of first-order logic
wenzelm@33873
    14
with equality, linear and nonlinear (natural/integer/real) arithmetic,
wenzelm@33873
    15
and fixed-size bitvectors.
haftmann@33866
    16
haftmann@33866
    17
* HOL-Boogie: an interactive prover back-end for Boogie and VCC.
haftmann@33866
    18
haftmann@33881
    19
* HOL: counterexample generator tool Nitpick based on the Kodkod
wenzelm@33873
    20
relational model finder.
wenzelm@33873
    21
wenzelm@33873
    22
* HOL: predicate compiler turning inductive into (executable)
wenzelm@33873
    23
equational specifications.
wenzelm@33873
    24
wenzelm@33873
    25
* HOL: refined number theory.
wenzelm@33873
    26
wenzelm@33873
    27
* HOL: various parts of multivariate analysis.
wenzelm@33873
    28
wenzelm@33873
    29
* HOLCF: new definitional domain package.
wenzelm@33873
    30
haftmann@33866
    31
* Revised tutorial on locales.
haftmann@33866
    32
wenzelm@33873
    33
* Support for Poly/ML 5.3.0, with improved reporting of compiler
wenzelm@33873
    34
errors and run-time exceptions, including detailed source positions.
haftmann@33866
    35
wenzelm@33873
    36
* Parallel checking of nested Isar proofs, with improved scalability
wenzelm@33873
    37
up to 8 cores.
wenzelm@33873
    38
wenzelm@12983
    39
wenzelm@33842
    40
You may get Isabelle2009-1 from the following mirror sites:
wenzelm@9928
    41
haftmann@27085
    42
  Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
haftmann@17696
    43
  Munich (Germany)     http://isabelle.in.tum.de/
kleing@14616
    44
  Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/