changeset 24340 | 811f78424efc |
parent 23467 | d1b97708d5eb |
child 32443 | 16464c3f86bd |
--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy Mon Aug 20 17:34:04 2007 +0200 +++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy Mon Aug 20 17:46:31 2007 +0200 @@ -5,7 +5,7 @@ header {* \isaheader{Welltyped Programs produce no Type Errors} *} -theory BVNoTypeError imports JVMDefensive BVSpecTypeSafe begin +theory BVNoTypeError imports "../JVM/JVMDefensive" BVSpecTypeSafe begin text {* Some simple lemmas about the type testing functions of the