--- a/src/HOL/MicroJava/BV/Correct.thy Wed Dec 02 12:04:07 2009 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy Tue Nov 24 14:37:23 2009 +0100
@@ -1,15 +1,13 @@
-
(* Title: HOL/MicroJava/BV/Correct.thy
- ID: $Id$
Author: Cornelia Pusch, Gerwin Klein
Copyright 1999 Technische Universitaet Muenchen
-
-The invariant for the type safety proof.
*)
header {* \isaheader{BV Type Safety Invariant} *}
-theory Correct imports BVSpec "../JVM/JVMExec" begin
+theory Correct
+imports BVSpec "../JVM/JVMExec"
+begin
constdefs
approx_val :: "[jvm_prog,aheap,val,ty err] \<Rightarrow> bool"