# 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] \ 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"];