--- a/src/HOL/MicroJava/README.html Tue Sep 26 17:07:28 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-<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 is
-<a href="http://isabelle.in.tum.de/Bali/papers/MOD99.html">available</a>.
-</BODY>
-</HTML>