changeset 9548 | 15bee2731e43 |
parent 1478 | 2b8c2a7547ab |
child 9654 | 9754ba005b64 |
--- a/src/ZF/CardinalArith.thy Mon Aug 07 10:29:04 2000 +0200 +++ b/src/ZF/CardinalArith.thy Mon Aug 07 10:29:54 2000 +0200 @@ -6,7 +6,7 @@ Cardinal Arithmetic *) -CardinalArith = Cardinal + OrderArith + Arith + Finite + +CardinalArith = Cardinal + OrderArith + ArithSimp + Finite + consts InfCard :: i=>o