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