src/HOL/Library/Cardinal_Notations.thy
author wenzelm
Sun Nov 02 17:20:45 2014 +0100 (2014-11-02)
changeset 58881 b9556a055632
parent 55128 6e16d2dd4f14
child 60500 903bb1495239
permissions -rw-r--r--
modernized header;
blanchet@55075
     1
(*  Title:      HOL/Library/Cardinal_Notations.thy
blanchet@55070
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@55070
     3
    Copyright   2013
blanchet@55070
     4
blanchet@55070
     5
Cardinal notations.
blanchet@55070
     6
*)
blanchet@55070
     7
wenzelm@58881
     8
section {* Cardinal Notations *}
blanchet@55070
     9
blanchet@55070
    10
theory Cardinal_Notations
blanchet@55070
    11
imports Main
blanchet@55070
    12
begin
blanchet@55070
    13
blanchet@55070
    14
notation
blanchet@55070
    15
  ordLeq2 (infix "<=o" 50) and
blanchet@55070
    16
  ordLeq3 (infix "\<le>o" 50) and
blanchet@55070
    17
  ordLess2 (infix "<o" 50) and
blanchet@55070
    18
  ordIso2 (infix "=o" 50) and
blanchet@55087
    19
  card_of ("|_|") and
blanchet@55128
    20
  BNF_Cardinal_Arithmetic.csum (infixr "+c" 65) and
blanchet@55128
    21
  BNF_Cardinal_Arithmetic.cprod (infixr "*c" 80) and
blanchet@55128
    22
  BNF_Cardinal_Arithmetic.cexp (infixr "^c" 90)
blanchet@55128
    23
blanchet@55128
    24
abbreviation "cinfinite \<equiv> BNF_Cardinal_Arithmetic.cinfinite"
blanchet@55128
    25
abbreviation "czero \<equiv> BNF_Cardinal_Arithmetic.czero"
blanchet@55128
    26
abbreviation "cone \<equiv> BNF_Cardinal_Arithmetic.cone"
blanchet@55128
    27
abbreviation "ctwo \<equiv> BNF_Cardinal_Arithmetic.ctwo"
blanchet@55070
    28
blanchet@55070
    29
end