code checking for Scala is mandatory, since Scala is now required anyway for Isabelle
authorhaftmann
Fri, 28 Dec 2012 10:25:59 +0100
changeset 50630 1ea90e8046dc
parent 50629 264ece81df93
child 50631 b69079c14665
code checking for Scala is mandatory, since Scala is now required anyway for Isabelle
src/HOL/Imperative_HOL/Imperative_HOL_ex.thy
src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
src/HOL/Imperative_HOL/ex/Linked_Lists.thy
--- a/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Fri Dec 28 10:15:39 2012 +0100
+++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Fri Dec 28 10:25:59 2012 +0100
@@ -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? Scala_imp?
+export_code everything checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_imp
 
 end
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Fri Dec 28 10:15:39 2012 +0100
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Fri Dec 28 10:25:59 2012 +0100
@@ -659,6 +659,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? Scala_imp?
+export_code qsort checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_imp
 
 end
--- 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
 
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Fri Dec 28 10:15:39 2012 +0100
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Fri Dec 28 10:25:59 2012 +0100
@@ -1000,7 +1000,7 @@
 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? Scala_imp?
+export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_imp
 
 end