--- a/src/HOL/Power.ML Fri Oct 05 21:50:37 2001 +0200
+++ b/src/HOL/Power.ML Fri Oct 05 21:52:39 2001 +0200
@@ -30,7 +30,7 @@
by Auto_tac;
qed "power_eq_0D";
-Goal "!!i::nat. 1 <= i ==> 1' <= i^n";
+Goal "!!i::nat. 1 <= i ==> Suc 0 <= i^n";
by (induct_tac "n" 1);
by Auto_tac;
qed "one_le_power";
@@ -49,12 +49,12 @@
by (asm_simp_tac (simpset() addsimps [power_add]) 1);
qed "le_imp_power_dvd";
-Goal "1 < i ==> \\<forall>n. i ^ m <= i ^ n --> m <= n";
+Goal "(1::nat) < i ==> \\<forall>n. i ^ m <= i ^ n --> m <= n";
by (induct_tac "m" 1);
by Auto_tac;
by (case_tac "na" 1);
by Auto_tac;
-by (subgoal_tac "2 * 1 <= i * i^n" 1);
+by (subgoal_tac "Suc 1 * 1 <= i * i^n" 1);
by (Asm_full_simp_tac 1);
by (rtac mult_le_mono 1);
by Auto_tac;
@@ -73,7 +73,7 @@
by (blast_tac (claset() addSDs [dvd_mult_right]) 1);
qed_spec_mp "power_le_dvd";
-Goal "[|i^m dvd i^n; 1 < i|] ==> m <= n";
+Goal "[|i^m dvd i^n; (1::nat) < i|] ==> m <= n";
by (rtac power_le_imp_le 1);
by (assume_tac 1);
by (etac dvd_imp_le 1);
@@ -120,7 +120,7 @@
qed "binomial_Suc_n";
Addsimps [binomial_Suc_n];
-Goal "(n choose 1') = n";
+Goal "(n choose Suc 0) = n";
by (induct_tac "n" 1);
by (ALLGOALS Asm_simp_tac);
qed "binomial_1";
@@ -162,8 +162,8 @@
qed "binomial_Suc_Suc_eq_times";
(*Another version, with -1 instead of Suc.*)
-Goal "[|k <= n; 0<k|] ==> (n choose k) * k = n * ((n-1) choose (k-1))";
-by (cut_inst_tac [("n","n-1"),("k","k-1")] Suc_times_binomial_eq 1);
+Goal "[|k <= n; 0<k|] ==> (n choose k) * k = n * ((n - 1) choose (k - 1))";
+by (cut_inst_tac [("n","n - 1"),("k","k - 1")] Suc_times_binomial_eq 1);
by (asm_full_simp_tac (simpset() addsplits [nat_diff_split]) 1);
by Auto_tac;
qed "times_binomial_minus1_eq";