# HG changeset patch
# User haftmann
# Date 1266826511 -3600
# Node ID 51692ec1b2201427869e4534b1cfde9ecd349eb2
# Parent  c283ae736beaa5706f3bb7fb3c872596e9893ec3
ascii syntax for multiset order

diff -r c283ae736bea -r 51692ec1b220 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Feb 22 09:15:10 2010 +0100
+++ b/src/HOL/Library/Multiset.thy	Mon Feb 22 09:15:11 2010 +0100
@@ -1206,11 +1206,14 @@
 
 subsubsection {* Partial-order properties *}
 
-definition less_multiset :: "'a\<Colon>order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subset>#" 50) where
-  "M' \<subset># M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
+definition less_multiset :: "'a\<Colon>order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<#" 50) where
+  "M' <# M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
 
-definition le_multiset :: "'a\<Colon>order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subseteq>#" 50) where
-  "M' \<subseteq># M \<longleftrightarrow> M' \<subset># M \<or> M' = M"
+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)
 
 interpretation multiset_order: order le_multiset less_multiset
 proof -