equal
deleted
inserted
replaced
1 (* ID: $Id$ *) |
1 (* ID: $Id$ *) |
2 (* EXTRACT from HOL/ex/Primes.thy*) |
2 (* EXTRACT from HOL/ex/Primes.thy*) |
3 |
3 |
4 (*Euclid's algorithm |
4 (*Euclid's algorithm |
5 This material now appears AFTER that of Forward.thy *) |
5 This material now appears AFTER that of Forward.thy *) |
6 theory Primes = Main: |
6 theory Primes imports Main begin |
7 consts |
7 consts |
8 gcd :: "nat*nat \<Rightarrow> nat" |
8 gcd :: "nat*nat \<Rightarrow> nat" |
9 |
9 |
10 recdef gcd "measure snd" |
10 recdef gcd "measure snd" |
11 "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))" |
11 "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))" |