src/HOL/Binomial.thy
changeset 17508 c84af7f39a6b
parent 16732 1bbe526a552c
child 19279 48b527d0331b
     1.1 --- a/src/HOL/Binomial.thy	Tue Sep 20 13:58:58 2005 +0200
     1.2 +++ b/src/HOL/Binomial.thy	Tue Sep 20 14:03:37 2005 +0200
     1.3 @@ -2,13 +2,12 @@
     1.4      ID:         $Id$
     1.5      Author:     Lawrence C Paulson
     1.6      Copyright   1997  University of Cambridge
     1.7 -
     1.8  *)
     1.9  
    1.10  header{*Binomial Coefficients*}
    1.11  
    1.12  theory Binomial
    1.13 -imports SetInterval
    1.14 +imports GCD
    1.15  begin
    1.16  
    1.17  text{*This development is based on the work of Andy Gordon and
    1.18 @@ -24,7 +23,7 @@
    1.19                   (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))"
    1.20  
    1.21  lemma binomial_n_0 [simp]: "(n choose 0) = 1"
    1.22 -by (case_tac "n", simp_all)
    1.23 +by (cases n) simp_all
    1.24  
    1.25  lemma binomial_0_Suc [simp]: "(0 choose Suc k) = 0"
    1.26  by simp
    1.27 @@ -188,21 +187,4 @@
    1.28    finally show ?case by simp
    1.29  qed
    1.30  
    1.31 -ML
    1.32 -{*
    1.33 -val binomial_n_0 = thm"binomial_n_0";
    1.34 -val binomial_0_Suc = thm"binomial_0_Suc";
    1.35 -val binomial_Suc_Suc = thm"binomial_Suc_Suc";
    1.36 -val binomial_eq_0 = thm"binomial_eq_0";
    1.37 -val binomial_n_n = thm"binomial_n_n";
    1.38 -val binomial_Suc_n = thm"binomial_Suc_n";
    1.39 -val binomial_1 = thm"binomial_1";
    1.40 -val zero_less_binomial = thm"zero_less_binomial";
    1.41 -val binomial_eq_0_iff = thm"binomial_eq_0_iff";
    1.42 -val zero_less_binomial_iff = thm"zero_less_binomial_iff";
    1.43 -val Suc_times_binomial_eq = thm"Suc_times_binomial_eq";
    1.44 -val binomial_Suc_Suc_eq_times = thm"binomial_Suc_Suc_eq_times";
    1.45 -val times_binomial_minus1_eq = thm"times_binomial_minus1_eq";
    1.46 -*}
    1.47 -
    1.48  end