changeset 54473 | 8bee5ca99e63 |
parent 52634 | 7c4b56bac189 |
child 54474 | 6d5941722fae |
--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy Mon Nov 18 18:04:44 2013 +0100 +++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy Mon Nov 18 18:04:44 2013 +0100 @@ -8,7 +8,7 @@ header {* Cardinal Arithmetic *} theory Cardinal_Arithmetic -imports Cardinal_Order_Relation_Base +imports Cardinal_Order_Relation_LFP begin text {*