src/HOL/GCD.thy
changeset 41792 ff3cb0c418b7
parent 41550 efa734d9b221
child 42871 1c0b99f950d9
     1.1 --- a/src/HOL/GCD.thy	Mon Feb 21 10:42:29 2011 +0100
     1.2 +++ b/src/HOL/GCD.thy	Mon Feb 21 10:44:19 2011 +0100
     1.3 @@ -1722,12 +1722,11 @@
     1.4  
     1.5  text{* Nitpick: *}
     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 +lemma gcd_eq_nitpick_gcd [nitpick_unfold]: "gcd x y = Nitpick.nat_gcd x y"
    1.12 +by (induct x y rule: nat_gcd.induct)
    1.13 +   (simp add: gcd_nat.simps Nitpick.nat_gcd.simps)
    1.14  
    1.15 -lemma lcm_eq_nitpick_lcm [nitpick_def]: "lcm x y \<equiv> Nitpick.nat_lcm x y"
    1.16 +lemma lcm_eq_nitpick_lcm [nitpick_unfold]: "lcm x y = Nitpick.nat_lcm x y"
    1.17  by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
    1.18  
    1.19  end