| 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)