| changeset 64586 | 1d25ca718790 |
| parent 64585 | 2155c0c1ecb6 |
| child 64587 | 8355a6e2df79 |
--- 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