# HG changeset patch
# User wenzelm
# Date 1187624791 -7200
# Node ID 811f78424efca591f4e3d921e30035040bf2b9ac
# Parent  d929e9b2e59820cb4d74bb1b08654ea7e1a29ca2
theory header: more precise imports;

diff -r d929e9b2e598 -r 811f78424efc src/HOL/MicroJava/BV/BVExample.thy
--- 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 {*
diff -r d929e9b2e598 -r 811f78424efc src/HOL/MicroJava/BV/BVNoTypeError.thy
--- 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
diff -r d929e9b2e598 -r 811f78424efc src/HOL/MicroJava/JVM/JVMListExample.thy
--- 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