src/HOL/MicroJava/BV/Altern.thy

--- a/src/HOL/MicroJava/BV/Altern.thy	Mon May 26 11:42:41 2003 +0200
+++ b/src/HOL/MicroJava/BV/Altern.thy	Mon May 26 18:36:15 2003 +0200
@@ -1,3 +1,13 @@
+(*  Title:      HOL/MicroJava/BV/Altern.thy
+    ID:         $Id$
+    Author:     Martin Strecker
+    Copyright   GPL 2003
+*)
+
+
+(* Alternative definition of well-typing of bytecode, 
+   used in compiler type correctness proof *)
+
 
 theory Altern = BVSpec: