src/HOL/Main.thy
changeset 63331 247eac9758dd
parent 62921 499a63c30d55
child 63655 d31650b377c4
--- a/src/HOL/Main.thy	Wed Jun 15 15:55:02 2016 +0200
+++ b/src/HOL/Main.thy	Fri Jun 17 09:44:16 2016 +0200
@@ -1,7 +1,7 @@
 section \<open>Main HOL\<close>
 
 theory Main
-imports Predicate_Compile Quickcheck_Narrowing Extraction Coinduction Nitpick BNF_Greatest_Fixpoint Filter
+imports Predicate_Compile Quickcheck_Narrowing Extraction Coinduction Nitpick BNF_Greatest_Fixpoint Filter Conditionally_Complete_Lattices
 begin
 
 text \<open>