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>