1.1 --- a/ANNOUNCE	Fri Oct 06 14:19:48 2000 +0200
     1.2 +++ b/ANNOUNCE	Fri Oct 06 15:15:19 2000 +0200
     1.3 @@ -2,12 +2,56 @@
     1.4  Subject: Announcing Isabelle99-1
     1.5  To: isabelle-users@cl.cam.ac.uk
     1.6  
     1.7 -Isabelle99-1 is now available.
     1.8 +Isabelle99-1 is now available.  This release continues the line of
     1.9 +Isabelle99, introducing numerous improvements, both internal and user
    1.10 +visible.
    1.11  
    1.12 +In particular, great care has been taken to improve robustness and
    1.13 +ease use and installation of the complete Isabelle working
    1.14 +environment, including the Proof General user interface support, WWW
    1.15 +presentation of theories and the Isabelle document preparation system.
    1.16  
    1.17 -The most prominent highlights are:
    1.18 +The most prominent highlights of Isabelle99-1 are as follows.
    1.19  
    1.20 -  *
    1.21 +  * Isabelle/Isar improvements (Markus Wenzel)
    1.22 +      o Support of tactic-emulation scripts for easy porting of legacy ML
    1.23 +        scripts (see also the HOL/Lambda example).
    1.24 +      o Better support for scalable verification tasks (manage large
    1.25 +        contexts in induction, generalized existence reasoning etc.)
    1.26 +      o Hindley-Milner polymorphism for proof texts.
    1.27 +      o More robust document preparation, better LaTeX output due to
    1.28 +        fake math-mode.
    1.29 +      o Extended "Isabelle/Isar Reference Manual"
    1.30 +        http://isabelle.in.tum.de/doc/isar-ref.pdf
    1.31 +
    1.32 +  * HOL/MicroJava (Gerwin Klein, Tobias Nipkow, David von Oheimb, and
    1.33 +    Cornelia Pusch)
    1.34 +    Formalization of a fragment of Java, together with a corresponding
    1.35 +    virtual machine and a specification of its bytecode verifier and a
    1.36 +    lightweight bytecode verifier, including proofs of type-safety.
    1.37 +
    1.38 +  * HOL/Real (Jacques Fleuriot)
    1.39 +    More on nonstandard real analysis.
    1.40 +
    1.41 +  * HOL/Algebra (Clemens Ballarin)
    1.42 +    Rings and univariate polynomials.
    1.43 +
    1.44 +  * HOL/NumberTheory (Thomas Rasmussen)
    1.45 +    Fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
    1.46 +    Fermat/Euler Theorem, Wilson's Theorem.
    1.47 +
    1.48 +  * HOL/Lambda (Stefan Berghofer and Tobias Nipkow)
    1.49 +    More on termination of simply-typed lambda-terms; converted into
    1.50 +    an Isabelle/Isar tactic emulation script.
    1.51 +
    1.52 +  * HOL/Lattice (Markus Wenzel)
    1.53 +    Lattices and orders in Isabelle/Isar.
    1.54 +
    1.55 +  * HOL/Isar_examples (Markus Wenzel)
    1.56 +    More examples, including a formulation of Hoare Logic in Isabelle/Isar.
    1.57 +
    1.58 +  * HOL/Prolog (David von Oheimb)
    1.59 +    A (bare-bones) implementation of Lambda-Prolog.
    1.60  
    1.61  See the NEWS file distributed with Isabelle for more details.
    1.62  
    1.63 @@ -16,5 +60,5 @@
    1.64  
    1.65    Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
    1.66    Munich (Germany)  http://isabelle.in.tum.de/dist/
    1.67 -  New Jersey (USA)  ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/source.html
    1.68 -  Stanford (USA)    ftp://rodin.stanford.edu/pub/smlnj/isabelle/source.html
    1.69 +  New Jersey (USA)  ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html
    1.70 +  Stanford (USA)    ftp://rodin.stanford.edu/pub/smlnj/isabelle/index.html