# HG changeset patch
# User haftmann
# Date 1280390219 -7200
# Node ID e4640c2ceb43e11c38d1471ec1bf2e34fcb3e15d
# Parent  5ac79735cfefe2d9a32ee91c94d18bab2151cd53
checking Scala_imp

diff -r 5ac79735cfef -r e4640c2ceb43 src/HOL/Imperative_HOL/Imperative_HOL_ex.thy
--- a/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Thu Jul 29 09:56:59 2010 +0200
+++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Thu Jul 29 09:56:59 2010 +0200
@@ -14,6 +14,6 @@
   Array.upd, Array.map_entry, Array.swap, Array.freeze,
   ref, Ref.lookup, Ref.update, Ref.change)"
 
-export_code everything checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala?
+export_code everything checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? Scala_imp?
 
 end
diff -r 5ac79735cfef -r e4640c2ceb43 src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Thu Jul 29 09:56:59 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Thu Jul 29 09:56:59 2010 +0200
@@ -655,6 +655,6 @@
 
 ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *}
 
-export_code qsort checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala?
+export_code qsort checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? Scala_imp?
 
 end
diff -r 5ac79735cfef -r e4640c2ceb43 src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
--- 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
diff -r 5ac79735cfef -r e4640c2ceb43 src/HOL/Imperative_HOL/ex/Linked_Lists.thy
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Thu Jul 29 09:56:59 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Thu Jul 29 09:56:59 2010 +0200
@@ -1014,6 +1014,6 @@
 ML {* @{code test_2} () *}
 ML {* @{code test_3} () *}
 
-export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala?
+export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? (*Scala_imp?*)
 
 end