# HG changeset patch
# User wenzelm
# Date 969982473 -7200
# Node ID 5245fa2ca8d37814a491e23191608fdaaa669db8
# Parent a9704bf900312f292fe94d0f3f7db51a83dda445
replaced by document (cannot maintain both);
diff -r a9704bf90031 -r 5245fa2ca8d3 src/HOL/MicroJava/README.html
--- 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 @@
-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 is
-available.
-
-