author  blanchet 
Thu, 23 Jan 2014 19:02:22 +0100  
changeset 55128  6e16d2dd4f14 
parent 55087  252c7fec4119 
child 58881  b9556a055632 
permissions  rwrr 
55075  1 
(* Title: HOL/Library/Cardinal_Notations.thy 
55070  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 

55087
252c7fec4119
renamed 'regular' to 'regularCard' to avoid clashes (e.g. in Meson_Test)
blanchet
parents:
55078
diff
changeset

19 
card_of ("_") and 
55128  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" 

55070  28 

29 
end 