src/HOL/Library/Cardinal_Notations.thy
changeset 55128 6e16d2dd4f14
parent 55087 252c7fec4119
child 58881 b9556a055632
     1.1 --- a/src/HOL/Library/Cardinal_Notations.thy	Thu Jan 23 16:09:28 2014 +0100
     1.2 +++ b/src/HOL/Library/Cardinal_Notations.thy	Thu Jan 23 19:02:22 2014 +0100
     1.3 @@ -17,8 +17,13 @@
     1.4    ordLess2 (infix "<o" 50) and
     1.5    ordIso2 (infix "=o" 50) and
     1.6    card_of ("|_|") and
     1.7 -  csum (infixr "+c" 65) and
     1.8 -  cprod (infixr "*c" 80) and
     1.9 -  cexp (infixr "^c" 90)
    1.10 +  BNF_Cardinal_Arithmetic.csum (infixr "+c" 65) and
    1.11 +  BNF_Cardinal_Arithmetic.cprod (infixr "*c" 80) and
    1.12 +  BNF_Cardinal_Arithmetic.cexp (infixr "^c" 90)
    1.13 +
    1.14 +abbreviation "cinfinite \<equiv> BNF_Cardinal_Arithmetic.cinfinite"
    1.15 +abbreviation "czero \<equiv> BNF_Cardinal_Arithmetic.czero"
    1.16 +abbreviation "cone \<equiv> BNF_Cardinal_Arithmetic.cone"
    1.17 +abbreviation "ctwo \<equiv> BNF_Cardinal_Arithmetic.ctwo"
    1.18  
    1.19  end