--- a/src/HOL/MicroJava/BV/Correct.thy Thu Mar 27 16:24:10 2008 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy Thu Mar 27 17:21:41 2008 +0100
@@ -9,7 +9,7 @@
header {* \isaheader{BV Type Safety Invariant} *}
-theory Correct imports BVSpec JVMExec begin
+theory Correct imports BVSpec "../JVM/JVMExec" begin
constdefs
approx_val :: "[jvm_prog,aheap,val,ty err] \<Rightarrow> bool"
--- a/src/HOLCF/IMP/Denotational.thy Thu Mar 27 16:24:10 2008 +0100
+++ b/src/HOLCF/IMP/Denotational.thy Thu Mar 27 17:21:41 2008 +0100
@@ -6,7 +6,7 @@
header "Denotational Semantics of Commands in HOLCF"
-theory Denotational imports HOLCF Natural begin
+theory Denotational imports HOLCF "../../HOL/IMP/Natural" begin
subsection "Definition"
--- a/src/HOLCF/IMP/ROOT.ML Thu Mar 27 16:24:10 2008 +0100
+++ b/src/HOLCF/IMP/ROOT.ML Thu Mar 27 17:21:41 2008 +0100
@@ -1,7 +1,3 @@
-(* Title: HOLCF/IMP/ROOT.ML
- ID: $Id$
- Author: Tobias Nipkow
- Copyright 1997 TU Muenchen
-*)
+(* $Id$ *)
-use_thys ["../../HOL/IMP/Natural", "HoareEx"];
+use_thys ["HoareEx"];