src/HOL/Library/Cardinal_Notations.thy
author blanchet
Wed Sep 24 15:45:55 2014 +0200 (2014-09-24)
changeset 58425 246985c6b20b
parent 55128 6e16d2dd4f14
child 58881 b9556a055632
permissions -rw-r--r--
simpler proof
     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   BNF_Cardinal_Arithmetic.csum (infixr "+c" 65) and
    21   BNF_Cardinal_Arithmetic.cprod (infixr "*c" 80) and
    22   BNF_Cardinal_Arithmetic.cexp (infixr "^c" 90)
    23 
    24 abbreviation "cinfinite \<equiv> BNF_Cardinal_Arithmetic.cinfinite"
    25 abbreviation "czero \<equiv> BNF_Cardinal_Arithmetic.czero"
    26 abbreviation "cone \<equiv> BNF_Cardinal_Arithmetic.cone"
    27 abbreviation "ctwo \<equiv> BNF_Cardinal_Arithmetic.ctwo"
    28 
    29 end