1.1 --- a/ANNOUNCE Mon Feb 05 14:30:55 2001 +0100
1.2 +++ b/ANNOUNCE Mon Feb 05 14:31:49 2001 +0100
1.3 @@ -1,63 +1,43 @@
1.4
1.5 -Subject: Announcing Isabelle99-1
1.6 +Subject: Announcing Isabelle99-2
1.7 To: isabelle-users@cl.cam.ac.uk
1.8
1.9 -Isabelle99-1 is now available. This release continues the line of
1.10 -Isabelle99, introducing numerous improvements, both internal and user
1.11 -visible.
1.12 +Isabelle99-2 is now available. This release continues the line of
1.13 +Isabelle99, introducing various improvements in robustness and
1.14 +usability.
1.15
1.16 -In particular, great care has been taken to improve robustness and
1.17 -ease use and installation of the complete Isabelle working
1.18 -environment. This includes Proof General user interface support, WWW
1.19 -presentation of theories and the Isabelle document preparation system.
1.20 -
1.21 -The most prominent highlights of Isabelle99-1 are as follows. See the
1.22 +The most prominent highlights of Isabelle99-2 are as follows. See the
1.23 NEWS file distributed with Isabelle for more details.
1.24
1.25 - * Isabelle/Isar improvements (Markus Wenzel)
1.26 - o Support of tactic-emulation scripts for easy porting of legacy ML
1.27 - scripts (see also the HOL/Lambda example).
1.28 - o Better support for scalable verification tasks (manage large
1.29 - contexts in induction, generalized existence reasoning etc.)
1.30 - o Hindley-Milner polymorphism for proof texts.
1.31 - o More robust document preparation, better LaTeX output due to
1.32 - fake math-mode.
1.33 - o Extended "Isabelle/Isar Reference Manual".
1.34 + * Poly/ML 4.0 used by default
1.35 + More robust, less disk space required.
1.36
1.37 - * HOL/Algebra (Clemens Ballarin)
1.38 - Rings and univariate polynomials.
1.39 + * Pure/Simplifier (Stefan Berghofer)
1.40 + Proper implementation as a derived rule, outside the kernel!
1.41
1.42 - * HOL/BCV (Tobias Nipkow)
1.43 - Generic model of bytecode verification.
1.44 + * Isabelle/Isar (Markus Wenzel)
1.45 + Numerous usability improvements, e.g. support for initial
1.46 + schematic goals, failure prediction of subgoal statements,
1.47 + handling of non-atomic statements in induction.
1.48
1.49 - * HOL/IMPP (David von Oheimb)
1.50 - Extension of IMP with local variables and mutually recursive procedures.
1.51 + * Improved document preparation (Markus Wenzel)
1.52 + Near math-mode, sub/super scripts, more symbols etc.
1.53
1.54 - * HOL/Isar_examples (Markus Wenzel)
1.55 - More examples, including a formulation of Hoare Logic in Isabelle/Isar.
1.56 + * HOL/Library (Gertrud Bauer, Tobias Nipkow, Lawrence C Paulson,
1.57 + Thomas M Rasmussen, Markus Wenzel)
1.58 + A collection of generic theories to be used together with main HOL.
1.59
1.60 - * HOL/Lambda (Stefan Berghofer and Tobias Nipkow)
1.61 - More on termination of simply-typed lambda-terms (Isar script).
1.62 + * HOL/Real and HOL/Hyperreal (Lawrence C Paulson and Jacques Fleuriot)
1.63 + General cleanup, more on nonstandard real analysis.
1.64
1.65 - * HOL/Lattice (Markus Wenzel)
1.66 - Lattices and orders in Isabelle/Isar.
1.67 + * HOL/Unix (Markus Wenzel)
1.68 + Some Aspects of Unix file-system security; demonstrates
1.69 + Isabelle/Isar in typical system modelling and verification tasks.
1.70
1.71 - * HOL/MicroJava (Gerwin Klein, Tobias Nipkow, David von Oheimb, and
1.72 - Cornelia Pusch)
1.73 - Formalization of a fragment of Java, together with a corresponding
1.74 - virtual machine and a specification of its bytecode verifier.
1.75 + * HOL/Tutorial (Tobias Nipkow, Lawrence C Paulson)
1.76 + Extended version of the Isabelle/HOL tutorial.
1.77
1.78 - * HOL/NumberTheory (Thomas Rasmussen)
1.79 - Fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
1.80 - Fermat/Euler Theorem, Wilson's Theorem.
1.81 -
1.82 - * HOL/Prolog (David von Oheimb)
1.83 - A (bare-bones) implementation of Lambda-Prolog.
1.84 -
1.85 - * HOL/Real (Jacques Fleuriot)
1.86 - More on nonstandard real analysis.
1.87 -
1.88 -You may get Isabelle99-1 from any of the following mirror sites:
1.89 +You may get Isabelle99-2 from any of the following mirror sites:
1.90
1.91 Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
1.92 Munich (Germany) http://isabelle.in.tum.de/dist/