# HG changeset patch
# User wenzelm
# Date 1206634901 -3600
# Node ID 090ced25100933a10596774539f53435331c4f73
# Parent  5906619c8c6b345fa4272f5b237478b4c4ccef5f
fixed theory imports;

diff -r 5906619c8c6b -r 090ced251009 src/HOL/MicroJava/BV/Correct.thy
--- 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"
diff -r 5906619c8c6b -r 090ced251009 src/HOLCF/IMP/Denotational.thy
--- 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"
 
diff -r 5906619c8c6b -r 090ced251009 src/HOLCF/IMP/ROOT.ML
--- 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"];