changeset 55056 | b5c94200d081 |
parent 55054 | e1f3714bc508 |
child 55057 | 6b0fcbeebaba |
--- a/src/HOL/Main.thy Mon Jan 20 18:24:55 2014 +0100 +++ b/src/HOL/Main.thy Mon Jan 20 18:24:55 2014 +0100 @@ -1,7 +1,7 @@ header {* Main HOL *} theory Main -imports Predicate_Compile Nitpick Extraction Lifting_Sum List_Prefix Coinduction Cardinal_Arithmetic_FP +imports Predicate_Compile Nitpick Extraction Lifting_Sum List_Prefix Coinduction BNF_Cardinal_Arithmetic begin text {*