# HG changeset patch
# User paulson
# Date 980760449 -3600
# Node ID 616bcfc7b8483cb74558502847b64f5cb0c6122a
# Parent  65a8a0e2d55bc876b91ef4120abfdfff1b42190f
simplified gcd

diff -r 65a8a0e2d55b -r 616bcfc7b848 doc-src/TutorialI/Rules/Primes.thy
--- 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))"