# HG changeset patch
# User haftmann
# Date 1216646785 -7200
# Node ID 2736967f27fdf5c197c8e9261af93c56251b597e
# Parent  52056ddac1942bfe93eaa31a08e75afcf46b6968
added code generation

diff -r 52056ddac194 -r 2736967f27fd src/HOL/ex/ImperativeQuicksort.thy
--- 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