replaced by document (cannot maintain both);
authorwenzelm
Tue Sep 26 17:34:33 2000 +0200 (2000-09-26)
changeset 100865245fa2ca8d3
parent 10085 a9704bf90031
child 10087 4dc7edfb0b5f
replaced by document (cannot maintain both);
src/HOL/MicroJava/README.html
     1.1 --- a/src/HOL/MicroJava/README.html	Tue Sep 26 17:07:28 2000 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,29 +0,0 @@
     1.4 -<HTML><HEAD><TITLE>HOL/MicroJava/README</TITLE></HEAD>
     1.5 -<BODY>
     1.6 -
     1.7 -<H1>Micro Java</H1>
     1.8 -
     1.9 -This theory defines Micro Java, a small fragment of the programming language
    1.10 -Java (essentially just classes), together with a corresponding virtual
    1.11 -machine and a specification of its bytecode verifier. It is shown that Micro
    1.12 -Java and the given specification of the bytecode verifier are type safe.
    1.13 -Directories:
    1.14 -<DL>
    1.15 -<DT>J
    1.16 -<DD>Micro Java
    1.17 -
    1.18 -<DT>JVM
    1.19 -<DD>The virtual machine
    1.20 -
    1.21 -<DT>BV
    1.22 -<DD>The bytecode verifier
    1.23 -
    1.24 -</DL>
    1.25 -
    1.26 -<P>
    1.27 -The theory was developed by David von Oheimb, Cornelia Pusch and Tobias
    1.28 -Nipkow as part of the DFG-funded project
    1.29 -<a href="http://isabelle.in.tum.de/bali/">Bali</a>. A publication is
    1.30 -<a href="http://isabelle.in.tum.de/Bali/papers/MOD99.html">available</a>.
    1.31 -</BODY>
    1.32 -</HTML>