src/HOL/Library/GCD.thy
changeset 27106 ff27dc6e7d05
parent 26304 02fbd0e7954a
child 27368 9f90ac19e32b
     1.1 --- a/src/HOL/Library/GCD.thy	Tue Jun 10 15:30:54 2008 +0200
     1.2 +++ b/src/HOL/Library/GCD.thy	Tue Jun 10 15:30:56 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 -  "is_gcd p m n \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
     1.8 +  [code func del]: "is_gcd p m n \<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 *}