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