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>