--- a/src/HOL/ex/ImperativeQuicksort.thy Mon Jul 21 15:26:24 2008 +0200
+++ b/src/HOL/ex/ImperativeQuicksort.thy Mon Jul 21 15:26:25 2008 +0200
@@ -1,5 +1,5 @@
theory ImperativeQuickSort
-imports Imperative_HOL Subarray Multiset
+imports Imperative_HOL Subarray Multiset Efficient_Nat
begin
text {* We prove QuickSort correct in the Relational Calculus. *}
@@ -619,4 +619,18 @@
done
qed
+
+subsection {* Example *}
+
+definition "qsort a = do
+ k \<leftarrow> length a;
+ quicksort a 0 (k - 1);
+ return a
+ done"
+
+ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *}
+
+export_code qsort in OCaml module_name Arr file -
+export_code qsort in Haskell module_name Arr file -
+
end
\ No newline at end of file