# HG changeset patch
# User boehmes
# Date 1265876048 -3600
# Node ID 1822c658a5e4e66b39dd83265aba7e0bb285ebaf
# Parent  cc7a0b9f938cd3795d38356dada45d813a1354cd
use full paths when importing theories

diff -r cc7a0b9f938c -r 1822c658a5e4 src/HOL/Boogie/Boogie.thy
--- a/src/HOL/Boogie/Boogie.thy	Thu Feb 11 00:45:02 2010 +0100
+++ b/src/HOL/Boogie/Boogie.thy	Thu Feb 11 09:14:08 2010 +0100
@@ -5,7 +5,7 @@
 header {* Integration of the Boogie program verifier *}
 
 theory Boogie
-imports SMT
+imports "~~/src/HOL/SMT/SMT"
 uses
   ("Tools/boogie_vcs.ML")
   ("Tools/boogie_loader.ML")
diff -r cc7a0b9f938c -r 1822c658a5e4 src/HOL/SMT/SMT_Base.thy
--- a/src/HOL/SMT/SMT_Base.thy	Thu Feb 11 00:45:02 2010 +0100
+++ b/src/HOL/SMT/SMT_Base.thy	Thu Feb 11 09:14:08 2010 +0100
@@ -5,7 +5,8 @@
 header {* SMT-specific definitions and basic tools *}
 
 theory SMT_Base
-imports Real Word "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
+imports Real "~~/src/HOL/Word/Word"
+  "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
 uses
   ("Tools/smt_normalize.ML")
   ("Tools/smt_monomorph.ML")