| changeset 29399 | ebcd69a00872 |
| parent 28145 | af3923ed4786 |
| child 29793 | 86cac1fab613 |
--- 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. *}