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