author  blanchet 
Mon, 20 Jan 2014 18:24:56 +0100  
changeset 55070  235c7661a96b 
permissions  rwrr 
55070  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 