# HG changeset patch
# User boehmes
# Date 1265876074 -3600
# Node ID a0334d7fb0abbdb18c30924cba78c349a1fab75f
# Parent  1822c658a5e4e66b39dd83265aba7e0bb285ebaf# Parent  5cf014192a6fa586031bf353e7b5c929a2080cb0
merged

diff -r 5cf014192a6f -r a0334d7fb0ab src/HOL/Boogie/Boogie.thy
--- a/src/HOL/Boogie/Boogie.thy	Thu Feb 11 08:44:41 2010 +0100
+++ b/src/HOL/Boogie/Boogie.thy	Thu Feb 11 09:14:34 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 5cf014192a6f -r a0334d7fb0ab src/HOL/SMT/SMT_Base.thy
--- a/src/HOL/SMT/SMT_Base.thy	Thu Feb 11 08:44:41 2010 +0100
+++ b/src/HOL/SMT/SMT_Base.thy	Thu Feb 11 09:14:34 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")