*** empty log message ***
Thu, 11 Nov 1999 12:44:08 +0100
changeset 8013 12f0ab3806c0
parent 8012 bbdf3c51c3b8
child 8014 fdf1281a3d0c
*** empty log message ***
--- /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 @@
+<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.
+<DD>Micro Java
+<DD>The virtual machine
+<DD>The bytecode verifier
+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.