1.1 --- a/ANNOUNCE	Fri Oct 06 17:22:15 2000 +0200
     1.2 +++ b/ANNOUNCE	Fri Oct 06 17:35:58 2000 +0200
     1.3 @@ -11,7 +11,8 @@
     1.4  environment.  This includes Proof General user interface support, WWW
     1.5  presentation of theories and the Isabelle document preparation system.
     1.6  
     1.7 -The most prominent highlights of Isabelle99-1 are as follows.
     1.8 +The most prominent highlights of Isabelle99-1 are as follows.  See the
     1.9 +NEWS file distributed with Isabelle for more details.
    1.10  
    1.11    * Isabelle/Isar improvements (Markus Wenzel)
    1.12        o Support of tactic-emulation scripts for easy porting of legacy ML
    1.13 @@ -27,19 +28,16 @@
    1.14      Rings and univariate polynomials.
    1.15  
    1.16    * HOL/BCV (Tobias Nipkow)
    1.17 -    Generic model of bytecode verification, i.e. data-flow
    1.18 -    analysis for assembly languages with subtypes.
    1.19 +    Generic model of bytecode verification.
    1.20  
    1.21    * HOL/IMPP (David von Oheimb)
    1.22 -    Extension of IMP with local variables and mutually recursive
    1.23 -    procedures.
    1.24 +    Extension of IMP with local variables and mutually recursive procedures.
    1.25  
    1.26    * HOL/Isar_examples (Markus Wenzel)
    1.27      More examples, including a formulation of Hoare Logic in Isabelle/Isar.
    1.28  
    1.29    * HOL/Lambda (Stefan Berghofer and Tobias Nipkow)
    1.30 -    More on termination of simply-typed lambda-terms; converted into
    1.31 -    an Isabelle/Isar tactic emulation script.
    1.32 +    More on termination of simply-typed lambda-terms (Isar script).
    1.33  
    1.34    * HOL/Lattice (Markus Wenzel)
    1.35      Lattices and orders in Isabelle/Isar.
    1.36 @@ -47,8 +45,7 @@
    1.37    * HOL/MicroJava (Gerwin Klein, Tobias Nipkow, David von Oheimb, and
    1.38      Cornelia Pusch)
    1.39      Formalization of a fragment of Java, together with a corresponding
    1.40 -    virtual machine and a specification of its bytecode verifier and a
    1.41 -    lightweight bytecode verifier, including proofs of type-safety.
    1.42 +    virtual machine and a specification of its bytecode verifier.
    1.43  
    1.44    * HOL/NumberTheory (Thomas Rasmussen)
    1.45      Fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
    1.46 @@ -60,10 +57,6 @@
    1.47    * HOL/Real (Jacques Fleuriot)
    1.48      More on nonstandard real analysis.
    1.49  
    1.50 -
    1.51 -See the NEWS file distributed with Isabelle for more details.
    1.52 -
    1.53 -
    1.54  You may get Isabelle99-1 from any of the following mirror sites:
    1.55  
    1.56    Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/