# HG changeset patch
# User blanchet
# Date 1428595258 -7200
# Node ID f38b94549dc83925495894cd92f91cb749f841be
# Parent  5574138cf97cd94164b74bb999ad4d61b5f2677b
introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)

diff -r 5574138cf97c -r f38b94549dc8 NEWS
--- 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.
diff -r 5574138cf97c -r f38b94549dc8 src/HOL/Library/Multiset.thy
--- 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)