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 {*