doc-src/Tutorial/Misc/GCD.thy

--- a/doc-src/Tutorial/Misc/GCD.thy	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-GCD = WF_Rel +
-consts gcd :: "nat*nat => nat"
-recdef gcd "measure ((%(m,n).n))"
-  simpset "simpset() addsimps [mod_less_divisor]"
-    "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
-end