src/HOL/ex/Numeral.thy
changeset 38773 f9837065b5e8
parent 38054 acd48ef85bfc
child 38797 abe92b33ac9f
--- a/src/HOL/ex/Numeral.thy	Thu Aug 26 10:23:25 2010 +0200
+++ b/src/HOL/ex/Numeral.thy	Thu Aug 26 12:19:49 2010 +0200
@@ -1033,14 +1033,14 @@
   (SML "IntInf.- ((_), 1)")
   (OCaml "Big'_int.pred'_big'_int")
   (Haskell "!(_/ -/ 1)")
-  (Scala "!(_/ -/ 1)")
+  (Scala "!(_ -/ 1)")
   (Eval "!(_/ -/ 1)")
 
 code_const Int.succ
   (SML "IntInf.+ ((_), 1)")
   (OCaml "Big'_int.succ'_big'_int")
   (Haskell "!(_/ +/ 1)")
-  (Scala "!(_/ +/ 1)")
+  (Scala "!(_ +/ 1)")
   (Eval "!(_/ +/ 1)")
 
 code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"