src/HOL/Algebra/AbelCoset.thy
changeset 40271 6014e8252e57
parent 39910 10097e0a9dbd
child 44655 fe0365331566
--- a/src/HOL/Algebra/AbelCoset.thy	Fri Oct 29 16:04:35 2010 +0200
+++ b/src/HOL/Algebra/AbelCoset.thy	Fri Oct 29 17:25:22 2010 +0200
@@ -13,7 +13,7 @@
 text {* Hiding @{text "<+>"} from @{theory Sum_Type} until I come
   up with better syntax here *}
 
-no_notation Plus (infixr "<+>" 65)
+no_notation Sum_Type.Plus (infixr "<+>" 65)
 
 definition
   a_r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "+>\<index>" 60)