--- a/src/HOL/Power.ML Tue May 23 12:44:03 2000 +0200
+++ b/src/HOL/Power.ML Tue May 23 18:06:22 2000 +0200
@@ -19,9 +19,9 @@
by (ALLGOALS (asm_simp_tac (simpset() addsimps [power_add])));
qed "power_mult";
-Goal "0 < i ==> 0 < i^n";
+Goal "!!i::nat. 0 < i ==> 0 < i^n";
by (induct_tac "n" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [zero_less_mult_iff])));
+by (ALLGOALS Asm_simp_tac);
qed "zero_less_power";
Addsimps [zero_less_power];
@@ -31,13 +31,13 @@
qed "one_le_power";
Addsimps [one_le_power];
-Goalw [dvd_def] "!!(m::nat) (i::nat). m<=n ==> i^m dvd i^n";
+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 "[| 0 < i; i^m < i^n |] ==> m<n";
+Goal "!!i::nat. [| 0 < i; i^m < i^n |] ==> m < n";
by (rtac ccontr 1);
by (dtac (leI RS le_imp_power_dvd RS dvd_imp_le RS leD) 1);
by (etac zero_less_power 1);