| changeset 4686 | 74a12e86b20b |
| parent 4356 | 0dfd34f0d33d |
| child 4728 | b72dd6b2ba56 |
--- a/src/HOL/ex/Primes.ML Fri Mar 06 18:25:28 1998 +0100 +++ b/src/HOL/ex/Primes.ML Sat Mar 07 16:29:29 1998 +0100 @@ -36,7 +36,7 @@ goal thy "!!m. 0<n ==> gcd(m,n) = gcd (n, m mod n)"; by (rtac (gcd_eq RS trans) 1); -by (asm_simp_tac (simpset() addsplits [expand_if]) 1); +by (Asm_simp_tac 1); by (Blast_tac 1); qed "gcd_less_0"; Addsimps [gcd_0, gcd_less_0];