--- a/ANNOUNCE Fri Oct 06 17:22:15 2000 +0200
+++ b/ANNOUNCE Fri Oct 06 17:35:58 2000 +0200
@@ -11,7 +11,8 @@
environment. This includes Proof General user interface support, WWW
presentation of theories and the Isabelle document preparation system.
-The most prominent highlights of Isabelle99-1 are as follows.
+The most prominent highlights of Isabelle99-1 are as follows. See the
+NEWS file distributed with Isabelle for more details.
* Isabelle/Isar improvements (Markus Wenzel)
o Support of tactic-emulation scripts for easy porting of legacy ML
@@ -27,19 +28,16 @@
Rings and univariate polynomials.
* HOL/BCV (Tobias Nipkow)
- Generic model of bytecode verification, i.e. data-flow
- analysis for assembly languages with subtypes.
+ Generic model of bytecode verification.
* HOL/IMPP (David von Oheimb)
- Extension of IMP with local variables and mutually recursive
- procedures.
+ Extension of IMP with local variables and mutually recursive procedures.
* 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
- an Isabelle/Isar tactic emulation script.
+ More on termination of simply-typed lambda-terms (Isar script).
* HOL/Lattice (Markus Wenzel)
Lattices and orders in Isabelle/Isar.
@@ -47,8 +45,7 @@
* 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.
+ virtual machine and a specification of its bytecode verifier.
* HOL/NumberTheory (Thomas Rasmussen)
Fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
@@ -60,10 +57,6 @@
* HOL/Real (Jacques Fleuriot)
More on nonstandard real analysis.
-
-See the NEWS file distributed with Isabelle for more details.
-
-
You may get Isabelle99-1 from any of the following mirror sites:
Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/