--- a/src/HOL/GCD.thy Fri Oct 23 18:57:35 2009 +0200
+++ b/src/HOL/GCD.thy Fri Oct 23 18:59:24 2009 +0200
@@ -1702,4 +1702,12 @@
show ?thesis by(simp add: Gcd_def fold_set gcd_commute_int)
qed
+lemma gcd_eq_nitpick_gcd [nitpick_def]: "gcd x y \<equiv> Nitpick.nat_gcd x y"
+apply (rule eq_reflection)
+apply (induct x y rule: nat_gcd.induct)
+by (simp add: gcd_nat.simps Nitpick.nat_gcd.simps)
+
+lemma lcm_eq_nitpick_lcm [nitpick_def]: "lcm x y \<equiv> Nitpick.nat_lcm x y"
+by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
+
end