# HG changeset patch
# User haftmann
# Date 1266908903 -3600
# Node ID 359e0fd38a92a0a760c8e0acefc6e8454ccfb94e
# Parent  8ee07543409fb9e17479a6c9572443bcefb63057
mind the "s"

diff -r 8ee07543409f -r 359e0fd38a92 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Feb 23 08:04:07 2010 +0100
+++ b/src/HOL/Library/Multiset.thy	Tue Feb 23 08:08:23 2010 +0100
@@ -1212,8 +1212,8 @@
 definition le_multiset :: "'a\<Colon>order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<=#" 50) where
   "M' <=# M \<longleftrightarrow> M' <# M \<or> M' = M"
 
-notation (xsymbol) less_multiset (infix "\<subset>#" 50)
-notation (xsymbol) le_multiset (infix "\<subseteq>#" 50)
+notation (xsymbols) less_multiset (infix "\<subset>#" 50)
+notation (xsymbols) le_multiset (infix "\<subseteq>#" 50)
 
 interpretation multiset_order: order le_multiset less_multiset
 proof -