| changeset 54480 | 57e781b711b5 |
| parent 54475 | b4d644be252c |
| child 54481 | 5c9819d7713b |
--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy Mon Nov 18 18:04:45 2013 +0100 +++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy Mon Nov 18 18:04:45 2013 +0100 @@ -8,7 +8,7 @@ header {* Cardinal Arithmetic *} theory Cardinal_Arithmetic -imports Cardinal_Arithmetic_GFP Cardinal_Order_Relation +imports Cardinal_Arithmetic_LFP Cardinal_Order_Relation begin