src/HOL/MicroJava/BV/BVSpecTypeSafe.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,10 @@
+(*  Title:      HOL/MicroJava/BV/BVSpecTypeSafe.thy
+    ID:         $Id$
+    Author:     Cornelia Pusch
+    Copyright   1999 Technische Universitaet Muenchen
+
+Proof that the specification of the bytecode verifier only admits type safe
+programs.
+*)
+
+BVSpecTypeSafe = Correct