author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 60500  903bb1495239 
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 

60500  8 
section \<open>Cardinal Notations\<close> 
55070  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 