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