--- a/src/HOL/BCV/README.html Fri Sep 01 18:01:05 2000 +0200
+++ b/src/HOL/BCV/README.html Fri Sep 01 18:29:52 2000 +0200
@@ -1,16 +1,17 @@
<HTML><HEAD><TITLE>HOL/BCV/README</TITLE></HEAD>
<BODY>
-<H1>Towards Verified Bytecode Verifiers</H1>
+<H1>Verified Bytecode Verifiers</H1>
-This theory defines a very abstract and generic model of bytecode
-verification, i.e. data-flow analysis for assembly languages with subtypes.
+This theory defines an abstract and generic model of bytecode
+verification, i.e. data-flow analysis for assembly languages with subtypes,
+and applies it to an equally abstract model of the JVM.
<P>
A paper describing the theory is found here:
-<A HREF = "http://www4.in.tum.de/~nipkow/pubs/bcv.html">
-Towards Verified Bytecode Verifiers</A>.
+<A HREF = "http://www.in.tum.de/~nipkow/pubs/bcv2.html">
+Verified Bytecode Verifiers</A>.
</BODY>
</HTML>