ANNOUNCE

--- a/ANNOUNCE	Fri Oct 06 15:15:19 2000 +0200
+++ b/ANNOUNCE	Fri Oct 06 16:11:53 2000 +0200
@@ -30,6 +30,10 @@
     virtual machine and a specification of its bytecode verifier and a
     lightweight bytecode verifier, including proofs of type-safety.
 
+  * 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.