src/HOL/Code_Numeral.thy
changeset 61857 542f2c6da692
parent 61275 053ec04ea866
child 63174 57c0d60e491c
     1.1 --- a/src/HOL/Code_Numeral.thy	Fri Dec 18 11:14:28 2015 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Fri Dec 18 14:23:11 2015 +0100
     1.3 @@ -648,6 +648,12 @@
     1.4      and (Haskell) infix 4 "<"
     1.5      and (Scala) infixl 4 "<"
     1.6      and (Eval) infixl 6 "<"
     1.7 +| constant "abs :: integer \<Rightarrow> _" \<rightharpoonup>
     1.8 +    (SML) "IntInf.abs"
     1.9 +    and (OCaml) "Big'_int.abs'_big'_int"
    1.10 +    and (Haskell) "Prelude.abs"
    1.11 +    and (Scala) "_.abs"
    1.12 +    and (Eval) "abs"
    1.13  
    1.14  code_identifier
    1.15    code_module Code_Numeral \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith