| changeset 55056 | b5c94200d081 |
| parent 54980 | 7e0573a490ee |
| child 55065 | 6d0af3c10864 |
--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy Mon Jan 20 18:24:55 2014 +0100 +++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy Mon Jan 20 18:24:55 2014 +0100 @@ -8,7 +8,7 @@ header {* Cardinal Arithmetic *} theory Cardinal_Arithmetic -imports Cardinal_Arithmetic_FP Cardinal_Order_Relation +imports BNF_Cardinal_Arithmetic Cardinal_Order_Relation begin subsection {* Binary sum *}