src/HOL/Binomial.thy

--- 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>