src/HOL/Cardinals/Cardinal_Notations.thy
changeset 55070 235c7661a96b
equal deleted inserted replaced
55069:b3e44be90122 55070:235c7661a96b
       
     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