equal
deleted
inserted
replaced
1 (* Title : Binomial.thy |
1 (* Title : Binomial.thy |
2 Author : Jacques D. Fleuriot |
2 Author : Jacques D. Fleuriot |
3 Copyright : 1998 University of Cambridge |
3 Copyright : 1998 University of Cambridge |
4 Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
4 Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
5 The integer version of factorial and other additions by Jeremy Avigad. |
5 Various additions by Jeremy Avigad. |
6 Additional binomial identities by Chaitanya Mangla and Manuel Eberl |
6 Additional binomial identities by Chaitanya Mangla and Manuel Eberl |
7 *) |
7 *) |
8 |
8 |
9 section\<open>Factorial Function, Binomial Coefficients and Binomial Theorem\<close> |
9 section\<open>Factorial Function, Binomial Coefficients and Binomial Theorem\<close> |
10 |
10 |