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