src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
changeset 50630 1ea90e8046dc
parent 47108 2a1953f0d20d
child 58889 5b7a9633cfa8
--- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Fri Dec 28 10:15:39 2012 +0100
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Fri Dec 28 10:25:59 2012 +0100
@@ -112,7 +112,7 @@
 
 definition "example = (Array.make 10 id \<guillemotright>= (\<lambda>a. rev a 0 9))"
 
-export_code example checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? Scala_imp?
+export_code example checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_imp
 
 end