# HG changeset patch
# User Andreas Lochbihler
# Date 1450444991 -3600
# Node ID 542f2c6da69262b7a75b017be91c6ee1e16025c7
# Parent  4b1b85f3894403abc93a1a27b932a487a10b46df
add serialisation for abs on integer to target language operation

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 \<Rightarrow> _" \<rightharpoonup>
+    (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 \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith