src/HOL/GCD.thy
changeset 33197 de6285ebcc05
parent 32960 69916a850301
child 33318 ddd97d9dfbfb
     1.1 --- a/src/HOL/GCD.thy	Fri Oct 23 18:57:35 2009 +0200
     1.2 +++ b/src/HOL/GCD.thy	Fri Oct 23 18:59:24 2009 +0200
     1.3 @@ -1702,4 +1702,12 @@
     1.4    show ?thesis by(simp add: Gcd_def fold_set gcd_commute_int)
     1.5  qed
     1.6  
     1.7 +lemma gcd_eq_nitpick_gcd [nitpick_def]: "gcd x y \<equiv> Nitpick.nat_gcd x y"
     1.8 +apply (rule eq_reflection)
     1.9 +apply (induct x y rule: nat_gcd.induct)
    1.10 +by (simp add: gcd_nat.simps Nitpick.nat_gcd.simps)
    1.11 +
    1.12 +lemma lcm_eq_nitpick_lcm [nitpick_def]: "lcm x y \<equiv> Nitpick.nat_lcm x y"
    1.13 +by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
    1.14 +
    1.15  end