src/HOL/Binomial.thy

--- a/src/HOL/Binomial.thy	Fri Jul 01 16:52:54 2016 +0200
+++ b/src/HOL/Binomial.thy	Sat Jul 02 08:41:05 2016 +0200
@@ -2,7 +2,7 @@
     Author      : Jacques D. Fleuriot
     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.
+    Various additions by Jeremy Avigad.
     Additional binomial identities by Chaitanya Mangla and Manuel Eberl
 *)