src/HOL/Code_Numeral.thy
changeset 37947 844977c7abeb
parent 36176 3fe7e97ccca8
child 37958 9728342bcd56
     1.1 --- a/src/HOL/Code_Numeral.thy	Fri Jul 23 10:25:00 2010 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Fri Jul 23 10:58:13 2010 +0200
     1.3 @@ -298,7 +298,7 @@
     1.4  code_type code_numeral
     1.5    (SML "int")
     1.6    (OCaml "Big'_int.big'_int")
     1.7 -  (Haskell "Int")
     1.8 +  (Haskell "Integer")
     1.9    (Scala "Int")
    1.10  
    1.11  code_instance code_numeral :: eq
    1.12 @@ -306,11 +306,9 @@
    1.13  
    1.14  setup {*
    1.15    fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
    1.16 -    false Code_Printer.literal_naive_numeral) ["SML", "Haskell"]
    1.17 -  #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
    1.18 -    false Code_Printer.literal_numeral "OCaml"
    1.19 -  #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
    1.20 -    false Code_Printer.literal_naive_numeral "Scala"
    1.21 +    false Code_Printer.literal_naive_numeral) ["SML", "Scala"]
    1.22 +  #> fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
    1.23 +    false Code_Printer.literal_numeral) ["OCaml", "Haskell"]
    1.24  *}
    1.25  
    1.26  code_reserved SML Int int
    1.27 @@ -325,7 +323,7 @@
    1.28  code_const "subtract_code_numeral \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
    1.29    (SML "Int.max/ (_/ -/ _,/ 0 : int)")
    1.30    (OCaml "Big'_int.max'_big'_int/ (Big'_int.sub'_big'_int/ _/ _)/ Big'_int.zero'_big'_int")
    1.31 -  (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
    1.32 +  (Haskell "max/ (_/ -/ _)/ (0 :: Integer)")
    1.33    (Scala "!(_/ -/ _).max(0)")
    1.34  
    1.35  code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"