ANNOUNCE

fix problem with user translations by making field names appear as consts;

Subject: Announcing Isabelle99-2
To: [e-mail]

Isabelle99-2 is now available.  This release continues the line of
Isabelle99, introducing various improvements in robustness and
usability.

The most prominent highlights of Isabelle99-2 are as follows.  See the
NEWS file distributed with Isabelle for more details.

  * Poly/ML 4.0 used by default
    More robust, less disk space required.

  * Simplifier (Stefan Berghofer)
    Proper implementation as a derived rule, outside the kernel!

  * Improved document preparation (Markus Wenzel)
    Near math-mode, sub/super scripts, more symbols etc.

  * Isabelle/Isar (Markus Wenzel)
    Numerous usability improvements, e.g. support for initial
    schematic goals, failure prediction of subgoal statements,
    handling of non-atomic statements in induction.

  * HOL/Library (Gertrud Bauer, Tobias Nipkow, Lawrence C Paulson,
      Thomas M Rasmussen, Markus Wenzel)
    A collection of generic theories to be used together with main HOL.

  * HOL/Real and HOL/Hyperreal (Jacques Fleuriot, Lawrence C Paulson)
    General cleanup, more on nonstandard real analysis.

  * HOL/Unix (Markus Wenzel)
    Some Aspects of Unix file-system security; demonstrates
    Isabelle/Isar in typical system modelling and verification tasks.

  * HOL/Tutorial (Tobias Nipkow, Lawrence C Paulson)
    Extended version of the Isabelle/HOL tutorial.

You may get Isabelle99-2 from any of the following mirror sites:

  Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
  Munich (Germany)  http://isabelle.in.tum.de/dist/
  New Jersey (USA)  ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html
  Stanford (USA)    ftp://rodin.stanford.edu/pub/smlnj/isabelle/index.html