# HG changeset patch
# User wenzelm
# Date 1213383849 -7200
# Node ID 005d4b953fdc7300a68447e7e1e36caf5bce67fd
# Parent  0fe5b95797da97109c8b53dc6efaee81989b7dc4
no_notation instead of hide;

diff -r 0fe5b95797da -r 005d4b953fdc src/HOL/Algebra/AbelCoset.thy
--- a/src/HOL/Algebra/AbelCoset.thy	Fri Jun 13 21:04:07 2008 +0200
+++ b/src/HOL/Algebra/AbelCoset.thy	Fri Jun 13 21:04:09 2008 +0200
@@ -16,7 +16,7 @@
 text {* Hiding @{text "<+>"} from @{theory Sum_Type} until I come
   up with better syntax here *}
 
-hide const Plus
+no_notation Plus (infixr "<+>" 65)
 
 constdefs (structure G)
   a_r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "+>\<index>" 60)