src/HOL/Library/Cardinal_Notations.thy
author blanchet
Mon Jan 20 18:59:53 2014 +0100 (2014-01-20)
changeset 55078 558c9ceabaa1
parent 55075 b3d0a02a756d
child 55087 252c7fec4119
permissions -rw-r--r--
deactivate one more cardinal notation
     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   card_of ("|_|" ) and
    20   csum (infixr "+c" 65) and
    21   cprod (infixr "*c" 80) and
    22   cexp (infixr "^c" 90)
    23 
    24 end