# HG changeset patch
# User wenzelm
# Date 970846558 7200
# Node ID 50be659d4222b68f95e9c966097e59091f26acf3
# Parent 4ede3a80e5e562264e457c56e8dceebd6324af64
final tuning;
diff r 4ede3a80e5e5 r 50be659d4222 ANNOUNCE
 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 Isabelle991 are as follows.
+The most prominent highlights of Isabelle991 are as follows. See the
+NEWS file distributed with Isabelle for more details.
* Isabelle/Isar improvements (Markus Wenzel)
o Support of tacticemulation 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. dataflow
 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 simplytyped lambdaterms; converted into
 an Isabelle/Isar tactic emulation script.
+ More on termination of simplytyped lambdaterms (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 typesafety.
+ 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 Isabelle991 from any of the following mirror sites:
Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/