no_notation instead of hide;
authorwenzelm
Fri Jun 13 21:04:09 2008 +0200 (2008-06-13)
changeset 27192005d4b953fdc
parent 27191 0fe5b95797da
child 27193 740159cfbf0e
no_notation instead of hide;
src/HOL/Algebra/AbelCoset.thy
     1.1 --- a/src/HOL/Algebra/AbelCoset.thy	Fri Jun 13 21:04:07 2008 +0200
     1.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Fri Jun 13 21:04:09 2008 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4  text {* Hiding @{text "<+>"} from @{theory Sum_Type} until I come
     1.5    up with better syntax here *}
     1.6  
     1.7 -hide const Plus
     1.8 +no_notation Plus (infixr "<+>" 65)
     1.9  
    1.10  constdefs (structure G)
    1.11    a_r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "+>\<index>" 60)