src/HOL/Ordinals_and_Cardinals/Wellorder_Embedding_Base.thy
changeset 48979 b62d14275b89
parent 48975 7f79f94a432c
--- a/src/HOL/Ordinals_and_Cardinals/Wellorder_Embedding_Base.thy	Tue Aug 28 17:17:41 2012 +0200
+++ b/src/HOL/Ordinals_and_Cardinals/Wellorder_Embedding_Base.thy	Tue Aug 28 17:19:59 2012 +0200
@@ -8,10 +8,7 @@
 header {* Well-Order Embeddings (Base) *}
 
 theory Wellorder_Embedding_Base
-imports
-  "~~/src/HOL/Library/Zorn"
-  Fun_More_Base
-  Wellorder_Relation_Base
+imports "~~/src/HOL/Library/Zorn" Fun_More_Base Wellorder_Relation_Base
 begin