Added attribute rulify_prems (useful for modifying premises of introduction
rules of inductive sets).
<HTML><HEAD><TITLE>HOL/BCV/README</TITLE></HEAD>
<BODY>
<H1>Towards 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.
<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>.
</BODY>
</HTML>