author | eberlm |
Tue, 03 Nov 2015 15:24:24 +0100 | |
changeset 61554 | 84901b8aa4f5 |
parent 61553 | 933eb9e6a1cc |
child 61564 | 6d513469f9b2 |
--- a/src/HOL/Binomial.thy Tue Nov 03 11:20:21 2015 +0100 +++ b/src/HOL/Binomial.thy Tue Nov 03 15:24:24 2015 +0100 @@ -3,6 +3,7 @@ Copyright : 1998 University of Cambridge Conversion to Isar and new proofs by Lawrence C Paulson, 2004 The integer version of factorial and other additions by Jeremy Avigad. + Additional binomial identities by Chaitanya Mangla and Manuel Eberl *) section\<open>Factorial Function, Binomial Coefficients and Binomial Theorem\<close>