changeset 54473 | 8bee5ca99e63 |
parent 49310 | 6e30078de4f0 |
child 54481 | 5c9819d7713b |
--- a/src/HOL/Cardinals/Wellorder_Embedding.thy Mon Nov 18 18:04:44 2013 +0100 +++ b/src/HOL/Cardinals/Wellorder_Embedding.thy Mon Nov 18 18:04:44 2013 +0100 @@ -8,7 +8,7 @@ header {* Well-Order Embeddings *} theory Wellorder_Embedding -imports Wellorder_Embedding_Base Fun_More Wellorder_Relation +imports Wellorder_Embedding_LFP Fun_More Wellorder_Relation begin