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