src/HOL/ex/Numeral.thy
changeset 39006 f9837065b5e8
parent 38300 acd48ef85bfc
child 39043 abe92b33ac9f
     1.1 --- a/src/HOL/ex/Numeral.thy	Thu Aug 26 10:23:25 2010 +0200
     1.2 +++ b/src/HOL/ex/Numeral.thy	Thu Aug 26 12:19:49 2010 +0200
     1.3 @@ -1033,14 +1033,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"