# HG changeset patch
# User eberlm
# Date 1446560664 -3600
# Node ID 84901b8aa4f5ec408285d602590813ac6972efe9
# Parent  933eb9e6a1cc19ea1ad17c4f07a716b3a6d8f1ef
added acknowledgement in Binomial.thy

diff -r 933eb9e6a1cc -r 84901b8aa4f5 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>