equal
deleted
inserted
replaced
34 by (Simp_tac 1); |
34 by (Simp_tac 1); |
35 qed "gcd_0"; |
35 qed "gcd_0"; |
36 |
36 |
37 goal thy "!!m. 0<n ==> gcd(m,n) = gcd (n, m mod n)"; |
37 goal thy "!!m. 0<n ==> gcd(m,n) = gcd (n, m mod n)"; |
38 by (rtac (gcd_eq RS trans) 1); |
38 by (rtac (gcd_eq RS trans) 1); |
39 by (asm_simp_tac (simpset() addsplits [expand_if]) 1); |
39 by (Asm_simp_tac 1); |
40 by (Blast_tac 1); |
40 by (Blast_tac 1); |
41 qed "gcd_less_0"; |
41 qed "gcd_less_0"; |
42 Addsimps [gcd_0, gcd_less_0]; |
42 Addsimps [gcd_0, gcd_less_0]; |
43 |
43 |
44 goal thy "gcd(m,0) dvd m"; |
44 goal thy "gcd(m,0) dvd m"; |