author | paulson |
Mon, 29 Jan 2001 10:27:29 +0100 | |
changeset 10986 | 616bcfc7b848 |
parent 10985 | 65a8a0e2d55b |
child 10987 | c36733b147e8 |
--- 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))"