1.1 --- a/ANNOUNCE	Fri Oct 06 17:18:35 2000 +0200
     1.2 +++ b/ANNOUNCE	Fri Oct 06 17:21:46 2000 +0200
     1.3 @@ -21,27 +21,21 @@
     1.4        o Hindley-Milner polymorphism for proof texts.
     1.5        o More robust document preparation, better LaTeX output due to
     1.6          fake math-mode.
     1.7 -      o Extended "Isabelle/Isar Reference Manual"
     1.8 +      o Extended "Isabelle/Isar Reference Manual".
     1.9  
    1.10 -  * HOL/MicroJava (Gerwin Klein, Tobias Nipkow, David von Oheimb, and
    1.11 -    Cornelia Pusch)
    1.12 -    Formalization of a fragment of Java, together with a corresponding
    1.13 -    virtual machine and a specification of its bytecode verifier and a
    1.14 -    lightweight bytecode verifier, including proofs of type-safety.
    1.15 +  * HOL/Algebra (Clemens Ballarin)
    1.16 +    Rings and univariate polynomials.
    1.17  
    1.18    * HOL/BCV (Tobias Nipkow)
    1.19      Generic model of bytecode verification, i.e. data-flow
    1.20      analysis for assembly languages with subtypes.
    1.21  
    1.22 -  * HOL/Real (Jacques Fleuriot)
    1.23 -    More on nonstandard real analysis.
    1.24 +  * HOL/IMPP (David von Oheimb)
    1.25 +    Extension of IMP with local variables and mutually recursive
    1.26 +    procedures.
    1.27  
    1.28 -  * HOL/Algebra (Clemens Ballarin)
    1.29 -    Rings and univariate polynomials.
    1.30 -
    1.31 -  * HOL/NumberTheory (Thomas Rasmussen)
    1.32 -    Fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
    1.33 -    Fermat/Euler Theorem, Wilson's Theorem.
    1.34 +  * HOL/Isar_examples (Markus Wenzel)
    1.35 +    More examples, including a formulation of Hoare Logic in Isabelle/Isar.
    1.36  
    1.37    * HOL/Lambda (Stefan Berghofer and Tobias Nipkow)
    1.38      More on termination of simply-typed lambda-terms; converted into
    1.39 @@ -50,12 +44,24 @@
    1.40    * HOL/Lattice (Markus Wenzel)
    1.41      Lattices and orders in Isabelle/Isar.
    1.42  
    1.43 -  * HOL/Isar_examples (Markus Wenzel)
    1.44 -    More examples, including a formulation of Hoare Logic in Isabelle/Isar.
    1.45 +  * HOL/MicroJava (Gerwin Klein, Tobias Nipkow, David von Oheimb, and
    1.46 +    Cornelia Pusch)
    1.47 +    Formalization of a fragment of Java, together with a corresponding
    1.48 +    virtual machine and a specification of its bytecode verifier and a
    1.49 +    lightweight bytecode verifier, including proofs of type-safety.
    1.50 +
    1.51 +  * HOL/NumberTheory (Thomas Rasmussen)
    1.52 +    Fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
    1.53 +    Fermat/Euler Theorem, Wilson's Theorem.
    1.54 +
    1.55 +  * HOL/Real (Jacques Fleuriot)
    1.56 +    More on nonstandard real analysis.
    1.57  
    1.58    * HOL/Prolog (David von Oheimb)
    1.59      A (bare-bones) implementation of Lambda-Prolog.
    1.60  
    1.61 +
    1.62 +
    1.63  See the NEWS file distributed with Isabelle for more details.
    1.64  
    1.65