src/HOL/Library/Cardinal_Notations.thy
author blanchet
Mon Jan 20 18:24:56 2014 +0100 (2014-01-20)
changeset 55075 b3d0a02a756d
parent 55070 src/HOL/Cardinals/Cardinal_Notations.thy@235c7661a96b
child 55078 558c9ceabaa1
permissions -rw-r--r--
dissolved BNF session
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
blanchet@55070
     8
header {* 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@55070
    19
  csum (infixr "+c" 65) and
blanchet@55070
    20
  cprod (infixr "*c" 80) and
blanchet@55070
    21
  cexp (infixr "^c" 90)
blanchet@55070
    22
blanchet@55070
    23
end