deactivate one more cardinal notation
authorblanchet
Mon Jan 20 18:59:53 2014 +0100 (2014-01-20)
changeset 55078558c9ceabaa1
parent 55077 4cf280104b85
child 55079 ec08a67e993b
deactivate one more cardinal notation
src/HOL/Library/Cardinal_Notations.thy
src/HOL/Main.thy
     1.1 --- a/src/HOL/Library/Cardinal_Notations.thy	Mon Jan 20 18:25:44 2014 +0100
     1.2 +++ b/src/HOL/Library/Cardinal_Notations.thy	Mon Jan 20 18:59:53 2014 +0100
     1.3 @@ -16,6 +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    csum (infixr "+c" 65) and
     1.9    cprod (infixr "*c" 80) and
    1.10    cexp (infixr "^c" 90)
     2.1 --- a/src/HOL/Main.thy	Mon Jan 20 18:25:44 2014 +0100
     2.2 +++ b/src/HOL/Main.thy	Mon Jan 20 18:59:53 2014 +0100
     2.3 @@ -27,6 +27,7 @@
     2.4    ordLeq3 (infix "\<le>o" 50) and
     2.5    ordLess2 (infix "<o" 50) and
     2.6    ordIso2 (infix "=o" 50) and
     2.7 +  card_of ("|_|") and
     2.8    csum (infixr "+c" 65) and
     2.9    cprod (infixr "*c" 80) and
    2.10    cexp (infixr "^c" 90)