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. *}