src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
changeset 37966 ac9bcae5ada7
parent 37959 6fe5fa827f18
child 38058 e4640c2ceb43
     1.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Mon Jul 26 11:09:44 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Mon Jul 26 11:09:45 2010 +0200
     1.3 @@ -655,6 +655,6 @@
     1.4  
     1.5  ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *}
     1.6  
     1.7 -export_code qsort checking SML SML_imp OCaml? OCaml_imp? Haskell? (*Scala?*)
     1.8 +export_code qsort checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala?
     1.9  
    1.10  end