src/HOL/Power.ML
changeset 11464 ddea204de5bc
parent 11365 6d5698df0413
child 11701 3d51fbf81c17
     1.1 --- a/src/HOL/Power.ML	Mon Aug 06 13:12:06 2001 +0200
     1.2 +++ b/src/HOL/Power.ML	Mon Aug 06 13:43:24 2001 +0200
     1.3 @@ -30,7 +30,7 @@
     1.4  by Auto_tac;  
     1.5  qed "power_eq_0D";
     1.6  
     1.7 -Goal "!!i::nat. 1 <= i ==> 1 <= i^n";
     1.8 +Goal "!!i::nat. 1 <= i ==> 1' <= i^n";
     1.9  by (induct_tac "n" 1);
    1.10  by Auto_tac;
    1.11  qed "one_le_power";
    1.12 @@ -120,7 +120,7 @@
    1.13  qed "binomial_Suc_n";
    1.14  Addsimps [binomial_Suc_n];
    1.15  
    1.16 -Goal "(n choose 1) = n";
    1.17 +Goal "(n choose 1') = n";
    1.18  by (induct_tac "n" 1);
    1.19  by (ALLGOALS Asm_simp_tac);
    1.20  qed "binomial_1";