src/HOL/Code_Numeral.thy
changeset 34898 62d70417f8ce
parent 34886 873c31d9f10d
child 34917 51829fe604a7
     1.1 --- a/src/HOL/Code_Numeral.thy	Wed Jan 13 12:20:37 2010 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Thu Jan 14 17:47:38 2010 +0100
     1.3 @@ -296,8 +296,11 @@
     1.4  
     1.5  setup {*
     1.6    fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
     1.7 -    false false) ["SML", "Haskell", "Scala"]
     1.8 -  #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral} false true "OCaml"
     1.9 +    false false Code_Printer.str) ["SML", "Haskell"]
    1.10 +  #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
    1.11 +    false true Code_Printer.str "OCaml"
    1.12 +  #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
    1.13 +    false false Code_Printer.str "Scala"
    1.14  *}
    1.15  
    1.16  code_reserved SML Int int
    1.17 @@ -323,9 +326,10 @@
    1.18    (Scala infixl 8 "*")
    1.19  
    1.20  code_const div_mod_code_numeral
    1.21 -  (SML "(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
    1.22 -  (OCaml "(fun k -> fun l ->/ Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int k)/ (Big'_int.abs'_big'_int l))")
    1.23 +  (SML "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
    1.24 +  (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
    1.25    (Haskell "divMod")
    1.26 +  (Scala "!((n: Int) => (m: Int) =>/ if (m == 0)/ (0, n) else/ (n '/ m, n % m))")
    1.27  
    1.28  code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
    1.29    (SML "!((_ : Int.int) = _)")
    1.30 @@ -337,12 +341,12 @@
    1.31    (SML "Int.<=/ ((_),/ (_))")
    1.32    (OCaml "Big'_int.le'_big'_int")
    1.33    (Haskell infix 4 "<=")
    1.34 -  (Scala infix 4 "<=")
    1.35 +  (Scala infixl 4 "<=")
    1.36  
    1.37  code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
    1.38    (SML "Int.</ ((_),/ (_))")
    1.39    (OCaml "Big'_int.lt'_big'_int")
    1.40    (Haskell infix 4 "<")
    1.41 -  (Scala infix 4 "<")
    1.42 +  (Scala infixl 4 "<")
    1.43  
    1.44  end