ANNOUNCE
author wenzelm
Thu Mar 07 23:21:19 2002 +0100 (2002-03-07)
changeset 13042 d8a345d9e067
parent 13010 3437d8d89803
child 13045 1db0bdda1d32
permissions -rw-r--r--
tuned;
wenzelm@9928
     1
wenzelm@12927
     2
Subject: Announcing Isabelle2002
wenzelm@9928
     3
To: isabelle-users@cl.cam.ac.uk
wenzelm@9928
     4
wenzelm@12927
     5
Isabelle2002 is now available.
wenzelm@12927
     6
wenzelm@12995
     7
This release provides major improvements.  The Isar language has
wenzelm@12995
     8
reached a mature state; the core engine is able to record full proof
wenzelm@12995
     9
terms; many aspects of the library have been reworked; several
wenzelm@12995
    10
substantial case studies have been added.  Some changes may cause
wenzelm@12995
    11
incompatibility with earlier versions, but improve accessibility of
wenzelm@12995
    12
Isabelle for new users.
wenzelm@12927
    13
wenzelm@12983
    14
The most prominent highlights of Isabelle2002 are as follows (see the
wenzelm@12983
    15
NEWS of the distribution for more details).
wenzelm@12964
    16
wenzelm@12995
    17
  * The Isabelle/HOL tutorial is to be published as LNCS 2283;
wenzelm@12983
    18
    Isabelle2002 is the official version to go along with that book
wenzelm@12983
    19
    (by Tobias Nipkow, Larry Paulson, Markus Wenzel).
wenzelm@12983
    20
wenzelm@13042
    21
  * Pure: explicit proof terms for all internal inferences;
wenzelm@12983
    22
    object-logics, proof tools etc. will benefit automatically
wenzelm@12983
    23
    (by Stefan Berghofer).
wenzelm@10161
    24
wenzelm@12983
    25
  * Pure/Isar: proper integration of the locale package for modular
wenzelm@12983
    26
    theory development; additional support for rename/merge
wenzelm@12983
    27
    operations, and type-inference for structured specifications
wenzelm@12983
    28
    (by Markus Wenzel).
wenzelm@12983
    29
wenzelm@13042
    30
  * Pure/Isar: streamlined cases/induction proof patterns
wenzelm@12983
    31
    (by Markus Wenzel).
wenzelm@12983
    32
wenzelm@12983
    33
  * Pure/HOL: infrastructure for generating functional and relational
wenzelm@13042
    34
    code, using the ML run-time environment
wenzelm@13042
    35
    (by Stefan Berghofer).
wenzelm@12983
    36
wenzelm@13042
    37
  * HOL/library: numerals on all number types; several improvements of
wenzelm@13042
    38
    tuple and record types; new definite description operator; keep
wenzelm@13042
    39
    Hilbert's epsilon (Axiom of Choice) out of basic theories
wenzelm@13042
    40
    (by Stefan Berghofer, Larry Paulson, Markus Wenzel).
wenzelm@12964
    41
wenzelm@12983
    42
  * HOL/Bali: large application concerning formal treatment of Java.
wenzelm@12983
    43
    (by David von Oheimb and Norbert Schirmer).
wenzelm@12983
    44
prensani@12996
    45
  * HOL/HoareParallel: large application concerning verification of
prensani@12996
    46
    parallel imperative programs (Owicki-Gries method, Rely-Guarantee
wenzelm@13042
    47
    method, examples of garbage collection, mutual exclusion)
wenzelm@12983
    48
    (by Leonor Prensa Nieto).
wenzelm@12983
    49
wenzelm@12983
    50
  * HOL/GroupTheory: group theory examples including Sylow's theorem
wenzelm@13042
    51
    (by Florian Kammueller).
wenzelm@9928
    52
wenzelm@13042
    53
  * HOL/IMP: several new proofs in Isar format
wenzelm@12983
    54
    (by Gerwin Klein).
wenzelm@12983
    55
kleing@13007
    56
  * HOL/MicroJava: exception handling on the bytecode level
kleing@13007
    57
    (by Gerwin Klein).
kleing@13007
    58
wenzelm@12983
    59
  * ZF/UNITY: typeless version of Chandy and Misra's formalism
wenzelm@12983
    60
    (by Sidi O Ehmety).
wenzelm@10162
    61
wenzelm@12983
    62
  * System: improvements and simplifications of document preparation
wenzelm@12983
    63
    (by Markus Wenzel).
wenzelm@12983
    64
wenzelm@12983
    65
  * System: support for Poly/ML 4.1.1 and PolyML/4.1.2, admitting
wenzelm@13042
    66
    larger heap size of applications; support for MacOS X (Poly/ML and
wenzelm@13042
    67
    SML/NJ).
wenzelm@10166
    68
wenzelm@12964
    69
You may get Isabelle2002 from any of the following mirror sites:
wenzelm@9928
    70
wenzelm@9928
    71
  Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
wenzelm@9928
    72
  Munich (Germany)  http://isabelle.in.tum.de/dist/
wenzelm@10161
    73
  New Jersey (USA)  ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html
wenzelm@10161
    74
  Stanford (USA)    ftp://rodin.stanford.edu/pub/smlnj/isabelle/index.html