src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
changeset 31873 00878e406bf5
parent 30689 b14b2cc4e25e
child 31887 b662352477c6
equal deleted inserted replaced
31872:a564aca741f2 31873:00878e406bf5
   629     return a
   629     return a
   630   done"
   630   done"
   631 
   631 
   632 ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *}
   632 ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *}
   633 
   633 
   634 export_code qsort in SML_imp module_name QSort
   634 (*export_code qsort in SML_imp module_name QSort*)
   635 export_code qsort in OCaml module_name QSort file -
   635 export_code qsort in OCaml module_name QSort file -
   636 export_code qsort in OCaml_imp module_name QSort file -
   636 (*export_code qsort in OCaml_imp module_name QSort file -*)
   637 export_code qsort in Haskell module_name QSort file -
   637 export_code qsort in Haskell module_name QSort file -
   638 
   638 
   639 end
   639 end