# HG changeset patch
# User wenzelm
# Date 970845706 -7200
# Node ID fb99cee36240fe2c0d5c51afe3edb0530355c25e
# Parent  eb69823db997b82d8ef90f47ac4e55ec986abcfe
tuned;

diff -r eb69823db997 -r fb99cee36240 ANNOUNCE
--- a/ANNOUNCE	Fri Oct 06 17:18:35 2000 +0200
+++ b/ANNOUNCE	Fri Oct 06 17:21:46 2000 +0200
@@ -21,27 +21,21 @@
       o Hindley-Milner polymorphism for proof texts.
       o More robust document preparation, better LaTeX output due to
         fake math-mode.
-      o Extended "Isabelle/Isar Reference Manual"
+      o Extended "Isabelle/Isar Reference Manual".
 
-  * HOL/MicroJava (Gerwin Klein, Tobias Nipkow, David von Oheimb, and
-    Cornelia Pusch)
-    Formalization of a fragment of Java, together with a corresponding
-    virtual machine and a specification of its bytecode verifier and a
-    lightweight bytecode verifier, including proofs of type-safety.
+  * HOL/Algebra (Clemens Ballarin)
+    Rings and univariate polynomials.
 
   * HOL/BCV (Tobias Nipkow)
     Generic model of bytecode verification, i.e. data-flow
     analysis for assembly languages with subtypes.
 
-  * HOL/Real (Jacques Fleuriot)
-    More on nonstandard real analysis.
+  * HOL/IMPP (David von Oheimb)
+    Extension of IMP with local variables and mutually recursive
+    procedures.
 
-  * HOL/Algebra (Clemens Ballarin)
-    Rings and univariate polynomials.
-
-  * HOL/NumberTheory (Thomas Rasmussen)
-    Fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
-    Fermat/Euler Theorem, Wilson's Theorem.
+  * HOL/Isar_examples (Markus Wenzel)
+    More examples, including a formulation of Hoare Logic in Isabelle/Isar.
 
   * HOL/Lambda (Stefan Berghofer and Tobias Nipkow)
     More on termination of simply-typed lambda-terms; converted into
@@ -50,12 +44,24 @@
   * HOL/Lattice (Markus Wenzel)
     Lattices and orders in Isabelle/Isar.
 
-  * HOL/Isar_examples (Markus Wenzel)
-    More examples, including a formulation of Hoare Logic in Isabelle/Isar.
+  * HOL/MicroJava (Gerwin Klein, Tobias Nipkow, David von Oheimb, and
+    Cornelia Pusch)
+    Formalization of a fragment of Java, together with a corresponding
+    virtual machine and a specification of its bytecode verifier and a
+    lightweight bytecode verifier, including proofs of type-safety.
+
+  * HOL/NumberTheory (Thomas Rasmussen)
+    Fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
+    Fermat/Euler Theorem, Wilson's Theorem.
+
+  * HOL/Real (Jacques Fleuriot)
+    More on nonstandard real analysis.
 
   * HOL/Prolog (David von Oheimb)
     A (bare-bones) implementation of Lambda-Prolog.
 
+
+
 See the NEWS file distributed with Isabelle for more details.