--- a/src/HOL/Imperative_HOL/Array.thy Tue Sep 15 15:22:15 2009 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy Tue Sep 15 15:41:23 2009 +0200
@@ -176,12 +176,11 @@
code_type array (OCaml "_/ array")
code_const Array (OCaml "failwith/ \"bare Array\"")
-code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ _/ _)")
+code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ (Big'_int.int'_of'_big'_int/ _)/ _)")
code_const Array.of_list (OCaml "(fun/ ()/ ->/ Array.of'_list/ _)")
-code_const Array.make' (OCaml "(fun/ ()/ ->/ Array.init/ _/ _)")
-code_const Array.length' (OCaml "(fun/ ()/ ->/ Array.length/ _)")
-code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ _)")
-code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ _/ _)")
+code_const Array.length' (OCaml "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))")
+code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))")
+code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)")
code_reserved OCaml Array
--- a/src/HOL/Imperative_HOL/ex/Sublist.thy Tue Sep 15 15:22:15 2009 +0200
+++ b/src/HOL/Imperative_HOL/ex/Sublist.thy Tue Sep 15 15:41:23 2009 +0200
@@ -1,4 +1,3 @@
-(* $Id$ *)
header {* Slices of lists *}
@@ -6,7 +5,6 @@
imports Multiset
begin
-
lemma sublist_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> sublist xs {i..<j} @ sublist xs {j..<k} = sublist xs {i..<k}"
apply (induct xs arbitrary: i j k)
apply simp