# HG changeset patch
# User haftmann
# Date 1467441665 -7200
# Node ID bd483ddb17f26fe1d9fb0a52b6c32d3fbe00dd1c
# Parent  9321740ae1d4ac05dd29c3d94da739f9e4f93c6d
more correct comment

diff -r 9321740ae1d4 -r bd483ddb17f2 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
 *)