# HG changeset patch
# User nipkow
# Date 942320648 -3600
# Node ID 12f0ab3806c08f510508f8e7e11abea54d845060
# Parent bbdf3c51c3b819119632b02029214424250acf5b
*** empty log message ***
diff -r bbdf3c51c3b8 -r 12f0ab3806c0 src/HOL/MicroJava/README.html
--- /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 @@
+HOL/MicroJava/README
+
+
+Micro Java
+
+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:
+
+- J
+
- Micro Java
+
+
- JVM
+
- The virtual machine
+
+
- BV
+
- The bytecode verifier
+
+
+
+
+The theory was developed by David von Oheimb, Cornelia Pusch and Tobias
+Nipkow as part of the DFG-funded project
+Bali. A publication on Micro
+Java is in preparation. Until it has appeared, please consult the Bali home
+page for publications.
+
+