| changeset 516 | 1957113f0d7d |
| parent 484 | 70b789956bd3 |
| child 753 | ec86863e87c8 |
| 515:abcc438e7c27 | 516:1957113f0d7d |
|---|---|
4 Copyright 1994 University of Cambridge |
4 Copyright 1994 University of Cambridge |
5 |
5 |
6 Cardinal Arithmetic |
6 Cardinal Arithmetic |
7 *) |
7 *) |
8 |
8 |
9 CardinalArith = Cardinal + OrderArith + Arith + Fin + |
9 CardinalArith = Cardinal + OrderArith + Arith + Finite + |
10 consts |
10 consts |
11 |
11 |
12 InfCard :: "i=>o" |
12 InfCard :: "i=>o" |
13 "|*|" :: "[i,i]=>i" (infixl 70) |
13 "|*|" :: "[i,i]=>i" (infixl 70) |
14 "|+|" :: "[i,i]=>i" (infixl 65) |
14 "|+|" :: "[i,i]=>i" (infixl 65) |