| 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