src/HOL/Library/Multiset.thy
changeset 59986 f38b94549dc8
parent 59958 4538d41e8e54
child 59997 90fb391a15c1
child 59998 c54d36be22ef
--- a/src/HOL/Library/Multiset.thy	Thu Apr 09 15:54:09 2015 +0200
+++ b/src/HOL/Library/Multiset.thy	Thu Apr 09 18:00:58 2015 +0200
@@ -295,6 +295,18 @@
 
 end
 
+abbreviation less_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<#" 50) where
+  "A <# B \<equiv> A < B"
+abbreviation (xsymbols) subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subset>#" 50) where
+  "A \<subset># B \<equiv> A < B"
+
+abbreviation less_eq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<=#" 50) where
+  "A <=# B \<equiv> A \<le> B"
+abbreviation (xsymbols) leq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<le>#" 50) where
+  "A \<le># B \<equiv> A \<le> B"
+abbreviation (xsymbols) subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subseteq>#" 50) where
+  "A \<subseteq># B \<equiv> A \<le> B"
+
 lemma mset_less_eqI:
   "(\<And>x. count A x \<le> count B x) \<Longrightarrow> A \<le> B"
   by (simp add: mset_le_def)