src/HOL/Cardinals/Cardinal_Arithmetic.thy

--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -11,12 +11,6 @@
 imports BNF_Cardinal_Arithmetic Cardinal_Order_Relation
 begin
 
-notation
-  csum (infixr "+c" 65) and
-  cprod (infixr "*c" 80) and
-  cexp (infixr "^c" 90)
-
-
 subsection {* Binary sum *}
 
 lemma csum_Cnotzero2: