src/HOL/Binomial.thy

--- 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>