author | haftmann |
Thu, 23 Jun 2016 16:46:36 +0200 | |
changeset 63351 | e5d08b1d8fea |
parent 63350 | 705229ed856e |
child 63354 | 6038ba2687cf |
--- 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