src/HOL/Code_Numeral.thy
changeset 69906 55534affe445
parent 69593 3dda49e08b9d
child 69946 494934c30f38
     1.1 --- a/src/HOL/Code_Numeral.thy	Sun Mar 10 15:16:45 2019 +0000
     1.2 +++ b/src/HOL/Code_Numeral.thy	Sun Mar 10 15:16:45 2019 +0000
     1.3 @@ -652,7 +652,7 @@
     1.4  code_printing
     1.5    type_constructor integer \<rightharpoonup>
     1.6      (SML) "IntInf.int"
     1.7 -    and (OCaml) "Big'_int.big'_int"
     1.8 +    and (OCaml) "Z.t"
     1.9      and (Haskell) "Integer"
    1.10      and (Scala) "BigInt"
    1.11      and (Eval) "int"
    1.12 @@ -662,7 +662,7 @@
    1.13  code_printing
    1.14    constant "0::integer" \<rightharpoonup>
    1.15      (SML) "!(0/ :/ IntInf.int)"
    1.16 -    and (OCaml) "Big'_int.zero'_big'_int"
    1.17 +    and (OCaml) "Z.zero"
    1.18      and (Haskell) "!(0/ ::/ Integer)"
    1.19      and (Scala) "BigInt(0)"
    1.20  
    1.21 @@ -676,25 +676,25 @@
    1.22  code_printing
    1.23    constant "plus :: integer \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
    1.24      (SML) "IntInf.+ ((_), (_))"
    1.25 -    and (OCaml) "Big'_int.add'_big'_int"
    1.26 +    and (OCaml) "Z.add"
    1.27      and (Haskell) infixl 6 "+"
    1.28      and (Scala) infixl 7 "+"
    1.29      and (Eval) infixl 8 "+"
    1.30  | constant "uminus :: integer \<Rightarrow> _" \<rightharpoonup>
    1.31      (SML) "IntInf.~"
    1.32 -    and (OCaml) "Big'_int.minus'_big'_int"
    1.33 +    and (OCaml) "Z.neg"
    1.34      and (Haskell) "negate"
    1.35      and (Scala) "!(- _)"
    1.36      and (Eval) "~/ _"
    1.37  | constant "minus :: integer \<Rightarrow> _" \<rightharpoonup>
    1.38      (SML) "IntInf.- ((_), (_))"
    1.39 -    and (OCaml) "Big'_int.sub'_big'_int"
    1.40 +    and (OCaml) "Z.sub"
    1.41      and (Haskell) infixl 6 "-"
    1.42      and (Scala) infixl 7 "-"
    1.43      and (Eval) infixl 8 "-"
    1.44  | constant Code_Numeral.dup \<rightharpoonup>
    1.45      (SML) "IntInf.*/ (2,/ (_))"
    1.46 -    and (OCaml) "Big'_int.mult'_big'_int/ (Big'_int.big'_int'_of'_int/ 2)"
    1.47 +    and (OCaml) "Z.shift'_left/ _/ 1"
    1.48      and (Haskell) "!(2 * _)"
    1.49      and (Scala) "!(2 * _)"
    1.50      and (Eval) "!(2 * _)"
    1.51 @@ -705,37 +705,37 @@
    1.52      and (Scala) "!sys.error(\"sub\")"
    1.53  | constant "times :: integer \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
    1.54      (SML) "IntInf.* ((_), (_))"
    1.55 -    and (OCaml) "Big'_int.mult'_big'_int"
    1.56 +    and (OCaml) "Z.mul"
    1.57      and (Haskell) infixl 7 "*"
    1.58      and (Scala) infixl 8 "*"
    1.59      and (Eval) infixl 9 "*"
    1.60  | constant Code_Numeral.divmod_abs \<rightharpoonup>
    1.61      (SML) "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)"
    1.62 -    and (OCaml) "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)"
    1.63 +    and (OCaml) "!(fun k l ->/ if Z.equal Z.zero l then/ (Z.zero, l) else/ Z.div'_rem/ (Z.abs k)/ (Z.abs l))"
    1.64      and (Haskell) "divMod/ (abs _)/ (abs _)"
    1.65      and (Scala) "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))"
    1.66      and (Eval) "Integer.div'_mod/ (abs _)/ (abs _)"
    1.67  | constant "HOL.equal :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
    1.68      (SML) "!((_ : IntInf.int) = _)"
    1.69 -    and (OCaml) "Big'_int.eq'_big'_int"
    1.70 +    and (OCaml) "Z.equal"
    1.71      and (Haskell) infix 4 "=="
    1.72      and (Scala) infixl 5 "=="
    1.73      and (Eval) infixl 6 "="
    1.74  | constant "less_eq :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
    1.75      (SML) "IntInf.<= ((_), (_))"
    1.76 -    and (OCaml) "Big'_int.le'_big'_int"
    1.77 +    and (OCaml) "Z.leq"
    1.78      and (Haskell) infix 4 "<="
    1.79      and (Scala) infixl 4 "<="
    1.80      and (Eval) infixl 6 "<="
    1.81  | constant "less :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
    1.82      (SML) "IntInf.< ((_), (_))"
    1.83 -    and (OCaml) "Big'_int.lt'_big'_int"
    1.84 +    and (OCaml) "Z.lt"
    1.85      and (Haskell) infix 4 "<"
    1.86      and (Scala) infixl 4 "<"
    1.87      and (Eval) infixl 6 "<"
    1.88  | constant "abs :: integer \<Rightarrow> _" \<rightharpoonup>
    1.89      (SML) "IntInf.abs"
    1.90 -    and (OCaml) "Big'_int.abs'_big'_int"
    1.91 +    and (OCaml) "Z.abs"
    1.92      and (Haskell) "Prelude.abs"
    1.93      and (Scala) "_.abs"
    1.94      and (Eval) "abs"