avoid overlapping equations for gcd, lcm on integers
authorhaftmann
Thu Jun 23 16:46:36 2016 +0200 (2016-06-23)
changeset 63351e5d08b1d8fea
parent 63350 705229ed856e
child 63354 6038ba2687cf
avoid overlapping equations for gcd, lcm on integers
src/HOL/Library/Code_Target_Int.thy
     1.1 --- a/src/HOL/Library/Code_Target_Int.thy	Thu Jun 23 16:46:36 2016 +0200
     1.2 +++ b/src/HOL/Library/Code_Target_Int.thy	Thu Jun 23 16:46:36 2016 +0200
     1.3 @@ -95,6 +95,8 @@
     1.4    "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
     1.5    by transfer rule
     1.6  
     1.7 +declare [[code drop: "gcd :: int \<Rightarrow> _" "lcm :: int \<Rightarrow> _"]]
     1.8 +
     1.9  lemma gcd_int_of_integer [code]:
    1.10    "gcd (int_of_integer x) (int_of_integer y) = int_of_integer (gcd x y)"
    1.11  by transfer rule