restored code generation for OCaml
authorhaftmann
Tue Sep 15 15:41:23 2009 +0200 (2009-09-15 ago)
changeset 325805b88ae4307ff
parent 32579 73ad5dbf1034
child 32581 44ac2e398411
restored code generation for OCaml
src/HOL/Imperative_HOL/Array.thy
src/HOL/Imperative_HOL/ex/Sublist.thy
     1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Tue Sep 15 15:22:15 2009 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Tue Sep 15 15:41:23 2009 +0200
     1.3 @@ -176,12 +176,11 @@
     1.4  
     1.5  code_type array (OCaml "_/ array")
     1.6  code_const Array (OCaml "failwith/ \"bare Array\"")
     1.7 -code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ _/ _)")
     1.8 +code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ (Big'_int.int'_of'_big'_int/ _)/ _)")
     1.9  code_const Array.of_list (OCaml "(fun/ ()/ ->/ Array.of'_list/ _)")
    1.10 -code_const Array.make' (OCaml "(fun/ ()/ ->/ Array.init/ _/ _)")
    1.11 -code_const Array.length' (OCaml "(fun/ ()/ ->/ Array.length/ _)")
    1.12 -code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ _)")
    1.13 -code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ _/ _)")
    1.14 +code_const Array.length' (OCaml "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))")
    1.15 +code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))")
    1.16 +code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)")
    1.17  
    1.18  code_reserved OCaml Array
    1.19  
     2.1 --- a/src/HOL/Imperative_HOL/ex/Sublist.thy	Tue Sep 15 15:22:15 2009 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/ex/Sublist.thy	Tue Sep 15 15:41:23 2009 +0200
     2.3 @@ -1,4 +1,3 @@
     2.4 -(* $Id$ *)
     2.5  
     2.6  header {* Slices of lists *}
     2.7  
     2.8 @@ -6,7 +5,6 @@
     2.9  imports Multiset
    2.10  begin
    2.11  
    2.12 -
    2.13  lemma sublist_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> sublist xs {i..<j} @ sublist xs {j..<k} = sublist xs {i..<k}" 
    2.14  apply (induct xs arbitrary: i j k)
    2.15  apply simp