# HG changeset patch
# User haftmann
# Date 1494612230 -7200
# Node ID bdd17b18e10356f7078ff1b1946d06995597bf85
# Parent  04ba6d530c87f5eeb6ddf391ae863ad19930fbca
relaxed theory dependencies

diff -r 04ba6d530c87 -r bdd17b18e103 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>
diff -r 04ba6d530c87 -r bdd17b18e103 src/HOL/Factorial.thy
--- 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>
diff -r 04ba6d530c87 -r bdd17b18e103 src/HOL/Main.thy
--- 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
diff -r 04ba6d530c87 -r bdd17b18e103 src/HOL/Pre_Main.thy
--- 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>