introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)

--- a/NEWS	Thu Apr 09 15:54:09 2015 +0200
+++ b/NEWS	Thu Apr 09 18:00:58 2015 +0200
@@ -338,6 +338,10 @@
       \<subset># ~> #\<subset>#
       \<subseteq># ~> #\<subseteq>#
     INCOMPATIBILITY.
+  - Introduced abbreviations for ill-named multiset operations:
+      <#, \<subset># abbreviate < (strict subset)
+      <=#, \<le>#, \<subseteq># abbreviate <= (subset or equal)
+    INCOMPATIBILITY.
   - Renamed
       in_multiset_of ~> in_multiset_in_set
     INCOMPATIBILITY.

--- 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)