| changeset 9637 | 47d39a31eb2f |
| parent 9424 | 234ef8652cae |
| child 11311 | 5a659c406465 |
--- a/src/HOL/Power.ML Thu Aug 17 12:01:09 2000 +0200 +++ b/src/HOL/Power.ML Thu Aug 17 12:02:01 2000 +0200 @@ -34,7 +34,6 @@ Goalw [dvd_def] "!!i::nat. m<=n ==> i^m dvd i^n"; by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1); by (asm_simp_tac (simpset() addsimps [power_add]) 1); -by (Blast_tac 1); qed "le_imp_power_dvd"; Goal "!!i::nat. [| 0 < i; i^m < i^n |] ==> m < n";