# HG changeset patch
# User paulson
# Date 939809264 -7200
# Node ID 6462cb4dfdc202a0d42d914c714a5eb747c623a6
# Parent  077d305615df32f2a9a1bc077b7b890609de7b72
deleted the redundant less_imp_binomial_eq_0

diff -r 077d305615df -r 6462cb4dfdc2 src/HOL/Power.ML
--- a/src/HOL/Power.ML	Wed Oct 13 12:07:23 1999 +0200
+++ b/src/HOL/Power.ML	Wed Oct 13 12:07:44 1999 +0200
@@ -71,16 +71,9 @@
 Addsimps [binomial_n_0, binomial_0_Suc, binomial_Suc_Suc];
 Delsimps [binomial_0, binomial_Suc];
 
-
-Goal "!k. n<k --> (n choose k) = 0";
-by (induct_tac "n" 1);
-by (ALLGOALS (rtac allI THEN' exhaust_tac "k"));
-by (ALLGOALS Asm_simp_tac);
-qed_spec_mp "less_imp_binomial_eq_0";
-
 Goal "(n choose n) = 1";
 by (induct_tac "n" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_imp_binomial_eq_0])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [binomial_eq_0])));
 qed "binomial_n_n";
 Addsimps [binomial_n_n];