src/HOL/Pre_Main.thy
changeset 65813 bdd17b18e103
parent 65552 f533820e7248
--- 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>