| changeset 10986 | 616bcfc7b848 |
| parent 10853 | 2c64c7991f7c |
| child 11080 | 22855d091249 |
--- a/doc-src/TutorialI/Rules/Primes.thy Sun Jan 28 16:46:19 2001 +0100 +++ b/doc-src/TutorialI/Rules/Primes.thy Mon Jan 29 10:27:29 2001 +0100 @@ -6,7 +6,7 @@ consts gcd :: "nat*nat \<Rightarrow> nat" -recdef gcd "measure ((\<lambda>(m,n).n) ::nat*nat \<Rightarrow> nat)" +recdef gcd "measure snd" "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"