src/HOL/Library/Code_Integer.thy
changeset 38773 f9837065b5e8
parent 38053 9102e859dc0b
child 38857 97775f3e8722
     1.1 --- a/src/HOL/Library/Code_Integer.thy	Thu Aug 26 10:23:25 2010 +0200
     1.2 +++ b/src/HOL/Library/Code_Integer.thy	Thu Aug 26 12:19:49 2010 +0200
     1.3 @@ -51,14 +51,14 @@
     1.4    (SML "IntInf.- ((_), 1)")
     1.5    (OCaml "Big'_int.pred'_big'_int")
     1.6    (Haskell "!(_/ -/ 1)")
     1.7 -  (Scala "!(_/ -/ 1)")
     1.8 +  (Scala "!(_ -/ 1)")
     1.9    (Eval "!(_/ -/ 1)")
    1.10  
    1.11  code_const Int.succ
    1.12    (SML "IntInf.+ ((_), 1)")
    1.13    (OCaml "Big'_int.succ'_big'_int")
    1.14    (Haskell "!(_/ +/ 1)")
    1.15 -  (Scala "!(_/ +/ 1)")
    1.16 +  (Scala "!(_ +/ 1)")
    1.17    (Eval "!(_/ +/ 1)")
    1.18  
    1.19  code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"