src/HOL/Main.thy
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 {*