src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
changeset 37959 6fe5fa827f18
parent 37845 b70d7a347964
child 37966 ac9bcae5ada7
     1.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Sat Jul 24 18:08:41 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Sat Jul 24 18:08:43 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