--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/README.html Thu Nov 11 12:44:08 1999 +0100
@@ -0,0 +1,30 @@
+<HTML><HEAD><TITLE>HOL/MicroJava/README</TITLE></HEAD>
+<BODY>
+
+<H1>Micro Java</H1>
+
+This theory defines Micro Java, a small fragment of the programming language
+Java (essentially just classes), together with a corresponding virtual
+machine and a specification of its bytecode verifier. It is shown that Micro
+Java and the given specification of the bytecode verifier are type safe.
+Directories:
+<DL>
+<DT>J
+<DD>Micro Java
+
+<DT>JVM
+<DD>The virtual machine
+
+<DT>BV
+<DD>The bytecode verifier
+
+</DL>
+
+<P>
+The theory was developed by David von Oheimb, Cornelia Pusch and Tobias
+Nipkow as part of the DFG-funded project
+<a href="http://isabelle.in.tum.de/bali/">Bali</a>. A publication on Micro
+Java is in preparation. Until it has appeared, please consult the Bali home
+page for publications.
+</BODY>
+</HTML>