| changeset 25691 | 8f8d83af100a |
| parent 25594 | 43c718438f9f |
| child 27368 | 9f90ac19e32b |
--- a/src/HOL/Library/Binomial.thy Tue Dec 18 12:26:24 2007 +0100 +++ b/src/HOL/Library/Binomial.thy Tue Dec 18 14:37:00 2007 +0100 @@ -7,7 +7,7 @@ header {* Binomial Coefficients *} theory Binomial -imports PreList +imports ATP_Linkup begin text {* This development is based on the work of Andy Gordon and