diff -r 4b1b85f38944 -r 542f2c6da692 src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Fri Dec 18 11:14:28 2015 +0100 +++ b/src/HOL/Code_Numeral.thy Fri Dec 18 14:23:11 2015 +0100 @@ -648,6 +648,12 @@ and (Haskell) infix 4 "<" and (Scala) infixl 4 "<" and (Eval) infixl 6 "<" +| constant "abs :: integer \ _" \ + (SML) "IntInf.abs" + and (OCaml) "Big'_int.abs'_big'_int" + and (Haskell) "Prelude.abs" + and (Scala) "_.abs" + and (Eval) "abs" code_identifier code_module Code_Numeral \ (SML) Arith and (OCaml) Arith and (Haskell) Arith