src/HOL/Library/Cardinal_Notations.thy
author blanchet
Mon Jan 20 18:24:56 2014 +0100 (2014-01-20)
changeset 55075 b3d0a02a756d
parent 55070 src/HOL/Cardinals/Cardinal_Notations.thy@235c7661a96b
child 55078 558c9ceabaa1
permissions -rw-r--r--
dissolved BNF session
     1 (*  Title:      HOL/Library/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