ANNOUNCE
author paulson
Wed Jul 25 13:13:01 2001 +0200 (2001-07-25)
changeset 11451 8abfb4f7bd02
parent 11109 ce1cefc6c14c
child 11600 bbd6268e0b4b
permissions -rw-r--r--
partial restructuring to reduce dependence on Axiom of Choice
wenzelm@9928
     1
wenzelm@11062
     2
Subject: Announcing Isabelle99-2
wenzelm@9928
     3
To: isabelle-users@cl.cam.ac.uk
wenzelm@9928
     4
wenzelm@11062
     5
Isabelle99-2 is now available.  This release continues the line of
wenzelm@11062
     6
Isabelle99, introducing various improvements in robustness and
wenzelm@11062
     7
usability.
wenzelm@10161
     8
wenzelm@11062
     9
The most prominent highlights of Isabelle99-2 are as follows.  See the
wenzelm@10168
    10
NEWS file distributed with Isabelle for more details.
wenzelm@9928
    11
wenzelm@11062
    12
  * Poly/ML 4.0 used by default
wenzelm@11062
    13
    More robust, less disk space required.
wenzelm@11062
    14
wenzelm@11109
    15
  * Simplifier (Stefan Berghofer)
wenzelm@11062
    16
    Proper implementation as a derived rule, outside the kernel!
wenzelm@9928
    17
wenzelm@11109
    18
  * Improved document preparation (Markus Wenzel)
wenzelm@11109
    19
    Near math-mode, sub/super scripts, more symbols etc.
wenzelm@11109
    20
wenzelm@11062
    21
  * Isabelle/Isar (Markus Wenzel)
wenzelm@11062
    22
    Numerous usability improvements, e.g. support for initial
wenzelm@11062
    23
    schematic goals, failure prediction of subgoal statements,
wenzelm@11062
    24
    handling of non-atomic statements in induction.
wenzelm@10162
    25
wenzelm@11062
    26
  * HOL/Library (Gertrud Bauer, Tobias Nipkow, Lawrence C Paulson,
wenzelm@11062
    27
      Thomas M Rasmussen, Markus Wenzel)
wenzelm@11062
    28
    A collection of generic theories to be used together with main HOL.
wenzelm@10161
    29
wenzelm@11109
    30
  * HOL/Real and HOL/Hyperreal (Jacques Fleuriot, Lawrence C Paulson)
wenzelm@11062
    31
    General cleanup, more on nonstandard real analysis.
wenzelm@10166
    32
wenzelm@11062
    33
  * HOL/Unix (Markus Wenzel)
wenzelm@11062
    34
    Some Aspects of Unix file-system security; demonstrates
wenzelm@11062
    35
    Isabelle/Isar in typical system modelling and verification tasks.
wenzelm@10166
    36
wenzelm@11062
    37
  * HOL/Tutorial (Tobias Nipkow, Lawrence C Paulson)
wenzelm@11062
    38
    Extended version of the Isabelle/HOL tutorial.
wenzelm@9928
    39
wenzelm@11062
    40
You may get Isabelle99-2 from any of the following mirror sites:
wenzelm@9928
    41
wenzelm@9928
    42
  Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
wenzelm@9928
    43
  Munich (Germany)  http://isabelle.in.tum.de/dist/
wenzelm@10161
    44
  New Jersey (USA)  ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html
wenzelm@10161
    45
  Stanford (USA)    ftp://rodin.stanford.edu/pub/smlnj/isabelle/index.html