--- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Thu Jul 29 09:56:59 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Thu Jul 29 09:56:59 2010 +0200
@@ -110,6 +110,8 @@
subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims)
(drule sym[of "List.length (Array.get h a)"], simp)
-export_code rev checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala?
+definition "example = (Array.of_list [1::nat, 2, 3, 4, 5, 6, 7, 8, 9, 10] \<guillemotright>= (\<lambda>a. rev a 0 9))"
+
+export_code example checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? Scala_imp?
end