| changeset 36176 | 3fe7e97ccca8 |
| parent 35712 | 77aa29bf14ee |
| child 36635 | 080b755377c0 |
--- a/src/HOL/Library/Multiset.thy Fri Apr 16 20:56:40 2010 +0200 +++ b/src/HOL/Library/Multiset.thy Fri Apr 16 21:28:09 2010 +0200 @@ -1001,7 +1001,7 @@ no_notation fcomp (infixl "o>" 60) no_notation scomp (infixl "o\<rightarrow>" 60) -hide (open) const bagify +hide_const (open) bagify subsection {* The multiset order *}