src/HOL/Library/Cardinal_Notations.thy
changeset 55087 252c7fec4119
parent 55078 558c9ceabaa1
child 55128 6e16d2dd4f14
     1.1 --- a/src/HOL/Library/Cardinal_Notations.thy	Mon Jan 20 21:45:08 2014 +0100
     1.2 +++ b/src/HOL/Library/Cardinal_Notations.thy	Mon Jan 20 22:24:48 2014 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4    ordLeq3 (infix "\<le>o" 50) and
     1.5    ordLess2 (infix "<o" 50) and
     1.6    ordIso2 (infix "=o" 50) and
     1.7 -  card_of ("|_|" ) and
     1.8 +  card_of ("|_|") and
     1.9    csum (infixr "+c" 65) and
    1.10    cprod (infixr "*c" 80) and
    1.11    cexp (infixr "^c" 90)