| changeset 55070 | 235c7661a96b |
| 55069:b3e44be90122 | 55070:235c7661a96b |
|---|---|
1 (* Title: HOL/Cardinals/Cardinal_Notations.thy |
|
2 Author: Jasmin Blanchette, TU Muenchen |
|
3 Copyright 2013 |
|
4 |
|
5 Cardinal notations. |
|
6 *) |
|
7 |
|
8 header {* Cardinal Notations *} |
|
9 |
|
10 theory Cardinal_Notations |
|
11 imports Main |
|
12 begin |
|
13 |
|
14 notation |
|
15 ordLeq2 (infix "<=o" 50) and |
|
16 ordLeq3 (infix "\<le>o" 50) and |
|
17 ordLess2 (infix "<o" 50) and |
|
18 ordIso2 (infix "=o" 50) and |
|
19 csum (infixr "+c" 65) and |
|
20 cprod (infixr "*c" 80) and |
|
21 cexp (infixr "^c" 90) |
|
22 |
|
23 end |