--- 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>
--- a/src/HOL/Factorial.thy Fri May 12 07:53:35 2017 +0200
+++ b/src/HOL/Factorial.thy Fri May 12 20:03:50 2017 +0200
@@ -9,7 +9,7 @@
section \<open>Factorial Function, Rising Factorials\<close>
theory Factorial
- imports Pre_Main
+ imports Groups_List
begin
subsection \<open>Factorial Function\<close>
--- a/src/HOL/Main.thy Fri May 12 07:53:35 2017 +0200
+++ b/src/HOL/Main.thy Fri May 12 20:03:50 2017 +0200
@@ -6,7 +6,7 @@
\<close>
theory Main
-imports Pre_Main GCD Binomial
+imports Pre_Main
begin
end
--- a/src/HOL/Pre_Main.thy Fri May 12 07:53:35 2017 +0200
+++ b/src/HOL/Pre_Main.thy Fri May 12 20:03:50 2017 +0200
@@ -1,7 +1,7 @@
section \<open>Main HOL\<close>
theory Pre_Main
-imports Predicate_Compile Quickcheck_Narrowing Extraction Nitpick BNF_Greatest_Fixpoint Filter Conditionally_Complete_Lattices
+imports Predicate_Compile Quickcheck_Narrowing Extraction Nitpick BNF_Greatest_Fixpoint Filter Conditionally_Complete_Lattices Binomial GCD
begin
text \<open>