diff -r 27676b51243d -r b7e8277fa088 src/HOL/README.html
--- a/src/HOL/README.html	Mon Oct 04 14:45:35 1999 +0200
+++ b/src/HOL/README.html	Mon Oct 04 21:34:20 1999 +0200
@@ -29,6 +29,10 @@
 
 </DL>
 
+<DT>BCV
+<DD>generic model of bytecode verification, i.e. data-flow analysis
+for assembly languages with subtypes.
+
 <DT>Hoare
 <DD>verification of imperative programs; verification conditions are
 generated automatically from pre/post conditions and loop invariants.