src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
changeset 38058 e4640c2ceb43
parent 37966 ac9bcae5ada7
child 40671 5e46057ba8e0
     1.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Thu Jul 29 09:56:59 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Thu Jul 29 09:56:59 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? Scala_imp?
     1.9  
    1.10  end