# HG changeset patch
# User haftmann
# Date 1466693196 -7200
# Node ID e5d08b1d8feaf5459e07fd11ec0faa822668419a
# Parent  705229ed856e5438174d73adbabf7ef20324a417
avoid overlapping equations for gcd, lcm on integers

diff -r 705229ed856e -r e5d08b1d8fea src/HOL/Library/Code_Target_Int.thy
--- a/src/HOL/Library/Code_Target_Int.thy	Thu Jun 23 16:46:36 2016 +0200
+++ b/src/HOL/Library/Code_Target_Int.thy	Thu Jun 23 16:46:36 2016 +0200
@@ -95,6 +95,8 @@
   "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
   by transfer rule
 
+declare [[code drop: "gcd :: int \<Rightarrow> _" "lcm :: int \<Rightarrow> _"]]
+
 lemma gcd_int_of_integer [code]:
   "gcd (int_of_integer x) (int_of_integer y) = int_of_integer (gcd x y)"
 by transfer rule