# HG changeset patch
# User blanchet
# Date 1453306493 -3600
# Node ID ad43b3ab06e49847ca82b9b0ce5f22be542f77af
# Parent  45eee631ea4f39d65589504e101c8cbd94865157
added 'supset' variants for new '<#' etc. symbols on multisets

diff -r 45eee631ea4f -r ad43b3ab06e4 NEWS
--- a/NEWS	Wed Jan 20 13:16:58 2016 +0100
+++ b/NEWS	Wed Jan 20 17:14:53 2016 +0100
@@ -648,10 +648,15 @@
 * Library/Multiset:
   - Renamed multiset inclusion operators:
       < ~> <#
+      > ~> >#
       \<subset> ~> \<subset>#
+      \<supset> ~> \<supset>#
       <= ~> <=#
+      >= ~> >=#
       \<le> ~> \<le>#
+      \<ge> ~> \<ge>#
       \<subseteq> ~> \<subseteq>#
+      \<supseteq> ~> \<supseteq>#
     INCOMPATIBILITY.
   - "'a multiset" is no longer an instance of the "order",
     "ordered_ab_semigroup_add_imp_le", "ordered_cancel_comm_monoid_diff",
diff -r 45eee631ea4f -r ad43b3ab06e4 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Jan 20 13:16:58 2016 +0100
+++ b/src/HOL/Library/Multiset.thy	Wed Jan 20 17:14:53 2016 +0100
@@ -271,12 +271,23 @@
 definition subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subset>#" 50)
   where "A \<subset># B = (A \<subseteq># B \<and> A \<noteq> B)"
 
+abbreviation (input) supseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
+  "supseteq_mset A B == B \<subseteq># A"
+
+abbreviation (input) supset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
+  "supset_mset A B == B \<subset># A"
+
 notation (input)
-  subseteq_mset  (infix "\<le>#" 50)
+  subseteq_mset  (infix "\<le>#" 50) and
+  supseteq_mset  (infix "\<ge>#" 50) and
+  supseteq_mset  (infix "\<supseteq>#" 50) and
+  supset_mset  (infix "\<supset>#" 50)
 
 notation (ASCII)
   subseteq_mset  (infix "<=#" 50) and
-  subset_mset  (infix "<#" 50)
+  subset_mset  (infix "<#" 50) and
+  supseteq_mset  (infix ">=#" 50) and
+  supset_mset  (infix ">#" 50)
 
 interpretation subset_mset: ordered_ab_semigroup_add_imp_le "op +" "op -" "op \<subseteq>#" "op \<subset>#"
   by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym)