equal
deleted
inserted
replaced
1 (* Title: HOL/Library/Cardinal_Notations.thy |
|
2 Author: Jasmin Blanchette, TU Muenchen |
|
3 Copyright 2013 |
|
4 |
|
5 Cardinal notations. |
|
6 *) |
|
7 |
|
8 section \<open>Cardinal Notations\<close> |
|
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 card_of ("|_|") and |
|
20 BNF_Cardinal_Arithmetic.csum (infixr "+c" 65) and |
|
21 BNF_Cardinal_Arithmetic.cprod (infixr "*c" 80) and |
|
22 BNF_Cardinal_Arithmetic.cexp (infixr "^c" 90) |
|
23 |
|
24 abbreviation "cinfinite \<equiv> BNF_Cardinal_Arithmetic.cinfinite" |
|
25 abbreviation "czero \<equiv> BNF_Cardinal_Arithmetic.czero" |
|
26 abbreviation "cone \<equiv> BNF_Cardinal_Arithmetic.cone" |
|
27 abbreviation "ctwo \<equiv> BNF_Cardinal_Arithmetic.ctwo" |
|
28 |
|
29 end |
|