| changeset 15339 | a7b603bbc1e6 |
| parent 15338 | 08519594b0e4 |
| child 15340 | cd18d7b73a64 |
| 15338:08519594b0e4 | 15339:a7b603bbc1e6 |
|---|---|
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 |