changeset 16417 | 9bc16273c2d4 |
parent 14883 | ca000a495448 |
child 24893 | b8ef7afe3a6b |
16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
---|---|
5 |
5 |
6 *) |
6 *) |
7 |
7 |
8 header{*Cardinal Arithmetic Without the Axiom of Choice*} |
8 header{*Cardinal Arithmetic Without the Axiom of Choice*} |
9 |
9 |
10 theory CardinalArith = Cardinal + OrderArith + ArithSimp + Finite: |
10 theory CardinalArith imports Cardinal OrderArith ArithSimp Finite begin |
11 |
11 |
12 constdefs |
12 constdefs |
13 |
13 |
14 InfCard :: "i=>o" |
14 InfCard :: "i=>o" |
15 "InfCard(i) == Card(i) & nat le i" |
15 "InfCard(i) == Card(i) & nat le i" |