| changeset 2034 | 5079fdf938dd |
| parent 1793 | 09fff2f0d727 |
| child 2469 | b50b8c0eec01 |
--- a/src/ZF/ex/Primes.ML Thu Sep 26 15:14:23 1996 +0200 +++ b/src/ZF/ex/Primes.ML Thu Sep 26 15:49:54 1996 +0200 @@ -51,7 +51,7 @@ (* GCD by Euclid's Algorithm *) goalw thy [egcd_def] "!!m. m:nat ==> egcd(m,0) = m"; -by (rtac (transrec RS ssubst) 1); +by (stac transrec 1); by (asm_simp_tac ZF_ss 1); qed "egcd_0";