src/HOL/Library/Code_Integer.thy
changeset 39006 f9837065b5e8
parent 38299 9102e859dc0b
child 39086 97775f3e8722
equal deleted inserted replaced
39005:eb7bc47f062b 39006:f9837065b5e8
    49 
    49 
    50 code_const Int.pred
    50 code_const Int.pred
    51   (SML "IntInf.- ((_), 1)")
    51   (SML "IntInf.- ((_), 1)")
    52   (OCaml "Big'_int.pred'_big'_int")
    52   (OCaml "Big'_int.pred'_big'_int")
    53   (Haskell "!(_/ -/ 1)")
    53   (Haskell "!(_/ -/ 1)")
    54   (Scala "!(_/ -/ 1)")
    54   (Scala "!(_ -/ 1)")
    55   (Eval "!(_/ -/ 1)")
    55   (Eval "!(_/ -/ 1)")
    56 
    56 
    57 code_const Int.succ
    57 code_const Int.succ
    58   (SML "IntInf.+ ((_), 1)")
    58   (SML "IntInf.+ ((_), 1)")
    59   (OCaml "Big'_int.succ'_big'_int")
    59   (OCaml "Big'_int.succ'_big'_int")
    60   (Haskell "!(_/ +/ 1)")
    60   (Haskell "!(_/ +/ 1)")
    61   (Scala "!(_/ +/ 1)")
    61   (Scala "!(_ +/ 1)")
    62   (Eval "!(_/ +/ 1)")
    62   (Eval "!(_/ +/ 1)")
    63 
    63 
    64 code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
    64 code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
    65   (SML "IntInf.+ ((_), (_))")
    65   (SML "IntInf.+ ((_), (_))")
    66   (OCaml "Big'_int.add'_big'_int")
    66   (OCaml "Big'_int.add'_big'_int")