src/HOL/Cardinals/Cardinal_Notations.thy
changeset 55070 235c7661a96b
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Cardinals/Cardinal_Notations.thy	Mon Jan 20 18:24:56 2014 +0100
     1.3 @@ -0,0 +1,23 @@
     1.4 +(*  Title:      HOL/Cardinals/Cardinal_Notations.thy
     1.5 +    Author:     Jasmin Blanchette, TU Muenchen
     1.6 +    Copyright   2013
     1.7 +
     1.8 +Cardinal notations.
     1.9 +*)
    1.10 +
    1.11 +header {* Cardinal Notations *}
    1.12 +
    1.13 +theory Cardinal_Notations
    1.14 +imports Main
    1.15 +begin
    1.16 +
    1.17 +notation
    1.18 +  ordLeq2 (infix "<=o" 50) and
    1.19 +  ordLeq3 (infix "\<le>o" 50) and
    1.20 +  ordLess2 (infix "<o" 50) and
    1.21 +  ordIso2 (infix "=o" 50) and
    1.22 +  csum (infixr "+c" 65) and
    1.23 +  cprod (infixr "*c" 80) and
    1.24 +  cexp (infixr "^c" 90)
    1.25 +
    1.26 +end