--- a/src/HOL/MicroJava/BV/BVExample.thy Mon Aug 20 17:34:04 2007 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy Mon Aug 20 17:46:31 2007 +0200
@@ -6,7 +6,7 @@
header {* \isaheader{Example Welltypings}\label{sec:BVExample} *}
theory BVExample
-imports JVMListExample BVSpecTypeSafe JVM Executable_Set
+imports "../JVM/JVMListExample" BVSpecTypeSafe "../JVM/JVM" Executable_Set
begin
text {*
--- 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
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy Mon Aug 20 17:34:04 2007 +0200
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy Mon Aug 20 17:46:31 2007 +0200
@@ -5,7 +5,7 @@
header {* \isaheader{Example for generating executable code from JVM semantics}\label{sec:JVMListExample} *}
-theory JVMListExample imports SystemClasses JVMExec begin
+theory JVMListExample imports "../J/SystemClasses" JVMExec begin
consts
list_nam :: cnam