
diff -r aab26a65e80f -r ebcd69a00872 src/HOL/ex/ImperativeQuicksort.thy
--- a/src/HOL/ex/ImperativeQuicksort.thy	Thu Jan 08 10:53:48 2009 +0100
+++ b/src/HOL/ex/ImperativeQuicksort.thy	Thu Jan 08 17:10:41 2009 +0100
@@ -1,5 +1,5 @@
 theory ImperativeQuicksort
-imports Imperative_HOL Subarray Multiset Efficient_Nat
+imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Subarray Multiset Efficient_Nat
 begin
 
 text {* We prove QuickSort correct in the Relational Calculus. *}




