doc-src/TutorialI/Rules/Primes.thy
changeset 35416 d8d7d1b785af
parent 33750 0a0d6d79d984
child 36745 403585a89772
     1.1 --- a/doc-src/TutorialI/Rules/Primes.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/doc-src/TutorialI/Rules/Primes.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -99,8 +99,7 @@
     1.4  
     1.5  (**** The material below was omitted from the book ****)
     1.6  
     1.7 -constdefs
     1.8 -  is_gcd  :: "[nat,nat,nat] \<Rightarrow> bool"        (*gcd as a relation*)
     1.9 +definition is_gcd :: "[nat,nat,nat] \<Rightarrow> bool" where        (*gcd as a relation*)
    1.10      "is_gcd p m n == p dvd m  \<and>  p dvd n  \<and>
    1.11                       (ALL d. d dvd m \<and> d dvd n \<longrightarrow> d dvd p)"
    1.12