changeset 55054 | e1f3714bc508 |
parent 55018 | 2a526bd279ed |
child 55056 | b5c94200d081 |
--- a/src/HOL/Main.thy Mon Jan 20 16:14:19 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 Zorn +imports Predicate_Compile Nitpick Extraction Lifting_Sum List_Prefix Coinduction Cardinal_Arithmetic_FP begin text {*