ANNOUNCE
author wenzelm
Sat Nov 28 17:59:02 2009 +0100 (2009-11-28)
changeset 33914 d17f447fec02
parent 33881 d8958955ecb5
child 37159 07f3f5a03e98
permissions -rw-r--r--
added "sos";
added subgoal focus;
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@33914
    29
* HOL-Library: proof method "sos" (sum of squares) for nonlinear real
wenzelm@33914
    30
arithmetic, based on external semidefinite programming solvers.
wenzelm@33914
    31
wenzelm@33873
    32
* HOLCF: new definitional domain package.
wenzelm@33873
    33
haftmann@33866
    34
* Revised tutorial on locales.
haftmann@33866
    35
wenzelm@33914
    36
* ML: tacticals for subgoal focus.
wenzelm@33914
    37
wenzelm@33914
    38
* ML: support for Poly/ML 5.3.0, with improved reporting of compiler
wenzelm@33873
    39
errors and run-time exceptions, including detailed source positions.
haftmann@33866
    40
wenzelm@33873
    41
* Parallel checking of nested Isar proofs, with improved scalability
wenzelm@33873
    42
up to 8 cores.
wenzelm@33873
    43
wenzelm@12983
    44
wenzelm@33842
    45
You may get Isabelle2009-1 from the following mirror sites:
wenzelm@9928
    46
haftmann@27085
    47
  Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
haftmann@17696
    48
  Munich (Germany)     http://isabelle.in.tum.de/
kleing@14616
    49
  Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/