changeset 65813 | bdd17b18e103 |
parent 65812 | 04ba6d530c87 |
child 66311 | 037aaa0b6daf |
--- a/src/HOL/Binomial.thy Fri May 12 07:53:35 2017 +0200 +++ b/src/HOL/Binomial.thy Fri May 12 20:03:50 2017 +0200 @@ -9,7 +9,7 @@ section \<open>Binomial Coefficients and Binomial Theorem\<close> theory Binomial - imports Factorial + imports Presburger Factorial begin subsection \<open>Binomial coefficients\<close>