src/HOL/Library/Cardinal_Notations.thy
author Manuel Eberl <eberlm@in.tum.de>
Mon Mar 26 16:14:16 2018 +0200 (18 months ago)
changeset 67951 655aa11359dc
parent 60500 903bb1495239
permissions -rw-r--r--
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
     1 (*  Title:      HOL/Library/Cardinal_Notations.thy
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2013
     4 
     5 Cardinal notations.
     6 *)
     7 
     8 section \<open>Cardinal Notations\<close>
     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