--- a/NEWS Mon Oct 04 14:45:35 1999 +0200
+++ b/NEWS Mon Oct 04 21:34:20 1999 +0200
@@ -170,6 +170,9 @@
* HOL/Real/HahnBanach: the Hahn-Banach theorem for real vector spaces
(in Isabelle/Isar) -- by Gertrud Bauer;
+* HOL/BCV: generic model of bytecode verification, i.e. data-flow
+analysis for assembly languages with subtypes;
+
* HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization
-- avoids syntactic ambiguities and treats state, transition, and
temporal levels more uniformly; introduces INCOMPATIBILITIES due to