src/HOL/Library/GCD.thy
changeset 28562 4e74209f113e
parent 27676 55676111ed69
     1.1 --- a/src/HOL/Library/GCD.thy	Fri Oct 10 06:45:50 2008 +0200
     1.2 +++ b/src/HOL/Library/GCD.thy	Fri Oct 10 06:45:53 2008 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4  
     1.5  definition
     1.6    is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where -- {* @{term gcd} as a relation *}
     1.7 -  [code func del]: "is_gcd m n p \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
     1.8 +  [code del]: "is_gcd m n p \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
     1.9      (\<forall>d. d dvd m \<longrightarrow> d dvd n \<longrightarrow> d dvd p)"
    1.10  
    1.11  text {* Uniqueness *}
    1.12 @@ -776,7 +776,7 @@
    1.13    thus ?thesis by (simp add: zlcm_def)
    1.14  qed
    1.15  
    1.16 -lemma zgcd_code [code func]:
    1.17 +lemma zgcd_code [code]:
    1.18    "zgcd k l = \<bar>if l = 0 then k else zgcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
    1.19    by (simp add: zgcd_def gcd.simps [of "nat \<bar>k\<bar>"] nat_mod_distrib)
    1.20