# HG changeset patch
# User haftmann
# Date 1481984520 -3600
# Node ID 1d25ca7187905f3a8bf1225c337774daccd688e6
# Parent  2155c0c1ecb6f785acf989e26ae311e18b34f264
redundant

diff -r 2155c0c1ecb6 -r 1d25ca718790 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat Dec 17 15:22:00 2016 +0100
+++ b/src/HOL/Library/Multiset.thy	Sat Dec 17 15:22:00 2016 +0100
@@ -887,11 +887,6 @@
   by (auto simp: multiset_eq_iff max_def)
 
 
-subsubsection \<open>Subset is an order\<close>
-
-interpretation subset_mset: order "op \<subseteq>#" "op \<subset>#" by unfold_locales
-
-
 subsection \<open>Replicate and repeat operations\<close>
 
 definition replicate_mset :: "nat \<Rightarrow> 'a \<Rightarrow> 'a multiset" where