src/HOL/Main.thy
changeset 58916 229765cc3414
parent 58889 5b7a9633cfa8
child 60036 218fcc645d22
--- a/src/HOL/Main.thy	Fri Nov 07 12:24:56 2014 +0100
+++ b/src/HOL/Main.thy	Fri Nov 07 11:28:37 2014 +0100
@@ -1,8 +1,7 @@
 section {* Main HOL *}
 
 theory Main
-imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick
-  BNF_Greatest_Fixpoint
+imports Predicate_Compile Quickcheck_Narrowing Extraction Coinduction Nitpick BNF_Greatest_Fixpoint
 begin
 
 text {*