src/HOL/Library/Code_Target_Int.thy
changeset 63351 e5d08b1d8fea
parent 61856 4b1b85f38944
child 64242 93c6f0da5c70
--- 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