# HG changeset patch # User haftmann # Date 1246373007 -7200 # Node ID b662352477c64b8e7aa96a1d0d7f60ff68b60f94 # Parent 3b08dcd74229cfaa77f8934e8136f7b9fa6981e6 restored diff -r 3b08dcd74229 -r b662352477c6 src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Tue Jun 30 14:54:32 2009 +0200 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Tue Jun 30 16:43:27 2009 +0200 @@ -631,9 +631,9 @@ ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *} -(*export_code qsort in SML_imp module_name QSort*) +export_code qsort in SML_imp module_name QSort export_code qsort in OCaml module_name QSort file - -(*export_code qsort in OCaml_imp module_name QSort file -*) +export_code qsort in OCaml_imp module_name QSort file - export_code qsort in Haskell module_name QSort file - end \ No newline at end of file