src/HOL/Main.thy
changeset 58128 43a1ba26a8cb
parent 58055 625bdd5c70b2
child 58152 6fe60a9a5bad
--- a/src/HOL/Main.thy	Mon Sep 01 16:34:39 2014 +0200
+++ b/src/HOL/Main.thy	Mon Sep 01 16:34:40 2014 +0200
@@ -1,7 +1,8 @@
 header {* Main HOL *}
 
 theory Main
-imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick BNF_GFP
+imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick
+  BNF_Greatest_Fixpoint
 begin
 
 text {*