author  blanchet 
Mon, 20 Jan 2014 22:24:48 +0100  
changeset 55087  252c7fec4119 
parent 55078  558c9ceabaa1 
child 55128  6e16d2dd4f14 
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 
55070  20 
csum (infixr "+c" 65) and 
21 
cprod (infixr "*c" 80) and 

22 
cexp (infixr "^c" 90) 

23 

24 
end 