ANNOUNCE
changeset 11062 e86340dc1d28
parent 10168 50be659d4222
child 11108 43791f99d71e
     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 +  * Pure/Simplifier (Stefan Berghofer)
    1.38 +    Proper implementation as a derived rule, outside the kernel!
    1.39  
    1.40 -  * HOL/Algebra (Clemens Ballarin)
    1.41 -    Rings and univariate polynomials.
    1.42 -
    1.43 -  * HOL/BCV (Tobias Nipkow)
    1.44 -    Generic model of bytecode verification.
    1.45 +  * Isabelle/Isar (Markus Wenzel)
    1.46 +    Numerous usability improvements, e.g. support for initial
    1.47 +    schematic goals, failure prediction of subgoal statements,
    1.48 +    handling of non-atomic statements in induction.
    1.49  
    1.50 -  * HOL/IMPP (David von Oheimb)
    1.51 -    Extension of IMP with local variables and mutually recursive procedures.
    1.52 -
    1.53 -  * HOL/Isar_examples (Markus Wenzel)
    1.54 -    More examples, including a formulation of Hoare Logic in Isabelle/Isar.
    1.55 +  * Improved document preparation (Markus Wenzel)
    1.56 +    Near math-mode, sub/super scripts, more symbols etc.
    1.57  
    1.58 -  * HOL/Lambda (Stefan Berghofer and Tobias Nipkow)
    1.59 -    More on termination of simply-typed lambda-terms (Isar script).
    1.60 +  * HOL/Library (Gertrud Bauer, Tobias Nipkow, Lawrence C Paulson,
    1.61 +      Thomas M Rasmussen, Markus Wenzel)
    1.62 +    A collection of generic theories to be used together with main HOL.
    1.63  
    1.64 -  * HOL/Lattice (Markus Wenzel)
    1.65 -    Lattices and orders in Isabelle/Isar.
    1.66 -
    1.67 -  * HOL/MicroJava (Gerwin Klein, Tobias Nipkow, David von Oheimb, and
    1.68 -    Cornelia Pusch)
    1.69 -    Formalization of a fragment of Java, together with a corresponding
    1.70 -    virtual machine and a specification of its bytecode verifier.
    1.71 +  * HOL/Real and HOL/Hyperreal (Lawrence C Paulson and Jacques Fleuriot)
    1.72 +    General cleanup, more on nonstandard real analysis.
    1.73  
    1.74 -  * HOL/NumberTheory (Thomas Rasmussen)
    1.75 -    Fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
    1.76 -    Fermat/Euler Theorem, Wilson's Theorem.
    1.77 +  * HOL/Unix (Markus Wenzel)
    1.78 +    Some Aspects of Unix file-system security; demonstrates
    1.79 +    Isabelle/Isar in typical system modelling and verification tasks.
    1.80  
    1.81 -  * HOL/Prolog (David von Oheimb)
    1.82 -    A (bare-bones) implementation of Lambda-Prolog.
    1.83 +  * HOL/Tutorial (Tobias Nipkow, Lawrence C Paulson)
    1.84 +    Extended version of the Isabelle/HOL tutorial.
    1.85  
    1.86 -  * HOL/Real (Jacques Fleuriot)
    1.87 -    More on nonstandard real analysis.
    1.88 -
    1.89 -You may get Isabelle99-1 from any of the following mirror sites:
    1.90 +You may get Isabelle99-2 from any of the following mirror sites:
    1.91  
    1.92    Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
    1.93    Munich (Germany)  http://isabelle.in.tum.de/dist/