NEWS
changeset 7691 b7e8277fa088
parent 7647 2ceddd91cd0a
child 7780 099742c562aa
--- 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