src/HOL/Library/Cardinal_Notations.thy
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (4 months ago)
changeset 69946 494934c30f38
parent 60500 903bb1495239
permissions -rw-r--r--
improved code equations taken over from AFP
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@60500
     8
section \<open>Cardinal Notations\<close>
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