| author | kleing |
| Sat, 19 Jan 2002 15:44:53 +0100 | |
| changeset 12818 | e7b4c0731d57 |
| parent 5377 | efb799c5ed3c |
| permissions | -rw-r--r-- |
| 5377 | 1 |
Goal "gcd(m,0) = m"; |
2 |
by(resolve_tac [trans] 1); |
|
3 |
by(resolve_tac gcd.rules 1); |
|
4 |
by(Simp_tac 1); |
|
5 |
qed "gcd_0"; |
|
6 |
Addsimps [gcd_0]; |
|
7 |
||
8 |
Goal "!!n. n ~= 0 ==> gcd(m,n) = gcd(n, m mod n)"; |
|
9 |
by(resolve_tac [trans] 1); |
|
10 |
by(resolve_tac gcd.rules 1); |
|
11 |
by(Asm_simp_tac 1); |
|
12 |
qed "gcd_not_0"; |
|
13 |
Addsimps [gcd_not_0]; |
|
14 |