# HG changeset patch
# User nipkow
# Date 1434722122 -7200
# Node ID 484559628038663be41e4cfcef6471e2f396438d
# Parent  78a82c37b4b25de6f2da9affca220668a62c48b7
renamed multiset_of -> mset

diff -r 78a82c37b4b2 -r 484559628038 NEWS
--- a/NEWS	Thu Jun 18 16:17:51 2015 +0200
+++ b/NEWS	Fri Jun 19 15:55:22 2015 +0200
@@ -116,8 +116,9 @@
     (e.g. add_mono ~> subset_mset.add_mono).
     INCOMPATIBILITY.
   - Renamed conversions:
+      multiset_of ~> mset
+      multiset_of_set ~> mset_set
       set_of ~> set_mset
-      multiset_of_set ~> mset_set
     INCOMPATIBILITY
   - Renamed lemmas:
       mset_le_def ~> subseteq_mset_def
diff -r 78a82c37b4b2 -r 484559628038 src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Thu Jun 18 16:17:51 2015 +0200
+++ b/src/HOL/Algebra/Divisibility.thy	Fri Jun 19 15:55:22 2015 +0200
@@ -1063,9 +1063,9 @@
   shows "P (set bs)"
 proof -
   from perm
-      have "multiset_of as = multiset_of bs"
-      by (simp add: multiset_of_eq_perm)
-  hence "set as = set bs" by (rule multiset_of_eq_setD)
+      have "mset as = mset bs"
+      by (simp add: mset_eq_perm)
+  hence "set as = set bs" by (rule mset_eq_setD)
   with as
       show "P (set bs)" by simp
 qed
@@ -1792,7 +1792,7 @@
   "assocs G x == eq_closure_of (division_rel G) {x}"
 
 definition
-  "fmset G as = multiset_of (map (\<lambda>a. assocs G a) as)"
+  "fmset G as = mset (map (\<lambda>a. assocs G a) as)"
 
 
 text {* Helper lemmas *}
@@ -1840,7 +1840,7 @@
   assumes prm: "as <~~> bs"
   shows "fmset G as = fmset G bs"
 using perm_map[OF prm]
-by (simp add: multiset_of_eq_perm fmset_def)
+by (simp add: mset_eq_perm fmset_def)
 
 lemma (in comm_monoid_cancel) eqc_listassoc_cong:
   assumes "as [\<sim>] bs"
@@ -1923,9 +1923,9 @@
     and p3: "map (assocs G) as <~~> map (assocs G) bs"
 
   from p1
-      have "multiset_of (map (assocs G) as) = multiset_of ys"
-      by (simp add: multiset_of_eq_perm)
-  hence setys: "set (map (assocs G) as) = set ys" by (rule multiset_of_eq_setD)
+      have "mset (map (assocs G) as) = mset ys"
+      by (simp add: mset_eq_perm)
+  hence setys: "set (map (assocs G) as) = set ys" by (rule mset_eq_setD)
 
   have "set (map (assocs G) as) = { assocs G x | x. x \<in> set as}" by clarsimp fast
   with setys have "set ys \<subseteq> { assocs G x | x. x \<in> set as}" by simp
@@ -1980,7 +1980,7 @@
 proof -
   from mset
       have mpp: "map (assocs G) as <~~> map (assocs G) bs"
-      by (simp add: fmset_def multiset_of_eq_perm)
+      by (simp add: fmset_def mset_eq_perm)
 
   have "\<exists>cas. cas = map (assocs G) as" by simp
   from this obtain cas where cas: "cas = map (assocs G) as" by simp
@@ -2003,7 +2003,7 @@
       and tm: "map (assocs G) as' = map (assocs G) bs"
       by auto
   from tm have lene: "length as' = length bs" by (rule map_eq_imp_length_eq)
-  from tp have "set as = set as'" by (simp add: multiset_of_eq_perm multiset_of_eq_setD)
+  from tp have "set as = set as'" by (simp add: mset_eq_perm mset_eq_setD)
   with ascarr
       have as'carr: "set as' \<subseteq> carrier G" by simp
 
@@ -2028,13 +2028,13 @@
   assumes elems: "\<And>X. X \<in> set_mset Cs \<Longrightarrow> \<exists>x. P x \<and> X = assocs G x"
   shows "\<exists>cs. (\<forall>c \<in> set cs. P c) \<and> fmset G cs = Cs"
 proof -
-  have "\<exists>Cs'. Cs = multiset_of Cs'"
-      by (rule surjE[OF surj_multiset_of], fast)
+  have "\<exists>Cs'. Cs = mset Cs'"
+      by (rule surjE[OF surj_mset], fast)
   from this obtain Cs'
-      where Cs: "Cs = multiset_of Cs'"
+      where Cs: "Cs = mset Cs'"
       by auto
 
-  have "\<exists>cs. (\<forall>c \<in> set cs. P c) \<and> multiset_of (map (assocs G) cs) = Cs"
+  have "\<exists>cs. (\<forall>c \<in> set cs. P c) \<and> mset (map (assocs G) cs) = Cs"
   using elems
   unfolding Cs
     apply (induct Cs', simp)
@@ -2042,7 +2042,7 @@
     fix a Cs' cs 
     assume ih: "\<And>X. X = a \<or> X \<in> set Cs' \<Longrightarrow> \<exists>x. P x \<and> X = assocs G x"
       and csP: "\<forall>x\<in>set cs. P x"
-      and mset: "multiset_of (map (assocs G) cs) = multiset_of Cs'"
+      and mset: "mset (map (assocs G) cs) = mset Cs'"
     from ih
         have "\<exists>x. P x \<and> a = assocs G x" by fast
     from this obtain c
@@ -2052,11 +2052,11 @@
     from cP csP
         have tP: "\<forall>x\<in>set (c#cs). P x" by simp
     from mset a
-    have "multiset_of (map (assocs G) (c#cs)) = multiset_of Cs' + {#a#}" by simp
+    have "mset (map (assocs G) (c#cs)) = mset Cs' + {#a#}" by simp
     from tP this
     show "\<exists>cs. (\<forall>x\<in>set cs. P x) \<and>
-               multiset_of (map (assocs G) cs) =
-               multiset_of Cs' + {#a#}" by fast
+               mset (map (assocs G) cs) =
+               mset Cs' + {#a#}" by fast
   qed
   thus ?thesis by (simp add: fmset_def)
 qed
diff -r 78a82c37b4b2 -r 484559628038 src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Thu Jun 18 16:17:51 2015 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Fri Jun 19 15:55:22 2015 +0200
@@ -34,11 +34,11 @@
 
 lemma swap_permutes:
   assumes "effect (swap a i j) h h' rs"
-  shows "multiset_of (Array.get h' a) 
-  = multiset_of (Array.get h a)"
+  shows "mset (Array.get h' a) 
+  = mset (Array.get h a)"
   using assms
   unfolding swap_def
-  by (auto simp add: Array.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: effect_bindE effect_nthE effect_returnE effect_updE)
+  by (auto simp add: Array.length_def mset_swap dest: sym [of _ "h'"] elim!: effect_bindE effect_nthE effect_returnE effect_updE)
 
 function part1 :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
 where
@@ -59,8 +59,8 @@
 
 lemma part_permutes:
   assumes "effect (part1 a l r p) h h' rs"
-  shows "multiset_of (Array.get h' a) 
-  = multiset_of (Array.get h a)"
+  shows "mset (Array.get h' a) 
+  = mset (Array.get h a)"
   using assms
 proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   case (1 a l r p h h' rs)
@@ -244,8 +244,8 @@
 
 lemma partition_permutes:
   assumes "effect (partition a l r) h h' rs"
-  shows "multiset_of (Array.get h' a) 
-  = multiset_of (Array.get h a)"
+  shows "mset (Array.get h' a) 
+  = mset (Array.get h a)"
 proof -
     from assms part_permutes swap_permutes show ?thesis
       unfolding partition.simps
@@ -424,8 +424,8 @@
 
 lemma quicksort_permutes:
   assumes "effect (quicksort a l r) h h' rs"
-  shows "multiset_of (Array.get h' a) 
-  = multiset_of (Array.get h a)"
+  shows "mset (Array.get h' a) 
+  = mset (Array.get h a)"
   using assms
 proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   case (1 a l r h h' rs)
@@ -533,23 +533,23 @@
         and part_conds2: "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h1) \<longrightarrow> Array.get h1 a ! p \<le> j"
         by (auto simp add: all_in_set_subarray_conv)
       from quicksort_outer_remains [OF qs1] quicksort_permutes [OF qs1] True
-        length_remains 1(5) pivot multiset_of_sublist [of l p "Array.get h1 a" "Array.get h2 a"]
-      have multiset_partconds1: "multiset_of (subarray l p a h2) = multiset_of (subarray l p a h1)"
+        length_remains 1(5) pivot mset_sublist [of l p "Array.get h1 a" "Array.get h2 a"]
+      have multiset_partconds1: "mset (subarray l p a h2) = mset (subarray l p a h1)"
         unfolding Array.length_def subarray_def by (cases p, auto)
       with left_subarray_remains part_conds1 pivot_unchanged
       have part_conds2': "\<forall>j. j \<in> set (subarray l p a h') \<longrightarrow> j \<le> Array.get h' a ! p"
-        by (simp, subst set_mset_multiset_of[symmetric], simp)
+        by (simp, subst set_mset_mset[symmetric], simp)
           (* -- These steps are the analogous for the right sublist \<dots> *)
       from quicksort_outer_remains [OF qs1] length_remains
       have right_subarray_remains: "subarray (p + 1) (r + 1) a h1 = subarray (p + 1) (r + 1) a h2"
         by (auto simp add: subarray_eq_samelength_iff)
       from quicksort_outer_remains [OF qs2] quicksort_permutes [OF qs2] True
-        length_remains 1(5) pivot multiset_of_sublist [of "p + 1" "r + 1" "Array.get h2 a" "Array.get h' a"]
-      have multiset_partconds2: "multiset_of (subarray (p + 1) (r + 1) a h') = multiset_of (subarray (p + 1) (r + 1) a h2)"
+        length_remains 1(5) pivot mset_sublist [of "p + 1" "r + 1" "Array.get h2 a" "Array.get h' a"]
+      have multiset_partconds2: "mset (subarray (p + 1) (r + 1) a h') = mset (subarray (p + 1) (r + 1) a h2)"
         unfolding Array.length_def subarray_def by auto
       with right_subarray_remains part_conds2 pivot_unchanged
       have part_conds1': "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h') \<longrightarrow> Array.get h' a ! p \<le> j"
-        by (simp, subst set_mset_multiset_of[symmetric], simp)
+        by (simp, subst set_mset_mset[symmetric], simp)
           (* -- Thirdly and finally, we show that the array is sorted
           following from the facts above. *)
       from True pivot 1(5) length_remains have "subarray l (r + 1) a h' = subarray l p a h' @ [Array.get h' a ! p] @ subarray (p + 1) (r + 1) a h'"
diff -r 78a82c37b4b2 -r 484559628038 src/HOL/Imperative_HOL/ex/Sublist.thy
--- a/src/HOL/Imperative_HOL/ex/Sublist.thy	Thu Jun 18 16:17:51 2015 +0200
+++ b/src/HOL/Imperative_HOL/ex/Sublist.thy	Fri Jun 19 15:55:22 2015 +0200
@@ -471,26 +471,26 @@
 unfolding set_sublist' by blast
 
 
-lemma multiset_of_sublist:
+lemma mset_sublist:
 assumes l_r: "l \<le> r \<and> r \<le> List.length xs"
 assumes left: "\<forall> i. i < l \<longrightarrow> (xs::'a list) ! i = ys ! i"
 assumes right: "\<forall> i. i \<ge> r \<longrightarrow> (xs::'a list) ! i = ys ! i"
-assumes multiset: "multiset_of xs = multiset_of ys"
-  shows "multiset_of (sublist' l r xs) = multiset_of (sublist' l r ys)"
+assumes multiset: "mset xs = mset ys"
+  shows "mset (sublist' l r xs) = mset (sublist' l r ys)"
 proof -
   from l_r have xs_def: "xs = (sublist' 0 l xs) @ (sublist' l r xs) @ (sublist' r (List.length xs) xs)" (is "_ = ?xs_long") 
     by (simp add: sublist'_append)
-  from multiset have length_eq: "List.length xs = List.length ys" by (rule multiset_of_eq_length)
+  from multiset have length_eq: "List.length xs = List.length ys" by (rule mset_eq_length)
   with l_r have ys_def: "ys = (sublist' 0 l ys) @ (sublist' l r ys) @ (sublist' r (List.length ys) ys)" (is "_ = ?ys_long") 
     by (simp add: sublist'_append)
-  from xs_def ys_def multiset have "multiset_of ?xs_long = multiset_of ?ys_long" by simp
+  from xs_def ys_def multiset have "mset ?xs_long = mset ?ys_long" by simp
   moreover
   from left l_r length_eq have "sublist' 0 l xs = sublist' 0 l ys"
     by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
   moreover
   from right l_r length_eq have "sublist' r (List.length xs) xs = sublist' r (List.length ys) ys"
     by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
-  ultimately show ?thesis by (simp add: multiset_of_append)
+  ultimately show ?thesis by (simp add: mset_append)
 qed
 
 
diff -r 78a82c37b4b2 -r 484559628038 src/HOL/Library/DAList_Multiset.thy
--- a/src/HOL/Library/DAList_Multiset.thy	Thu Jun 18 16:17:51 2015 +0200
+++ b/src/HOL/Library/DAList_Multiset.thy	Fri Jun 19 15:55:22 2015 +0200
@@ -267,7 +267,7 @@
 
 declare multiset_inter_def [code]
 declare sup_subset_mset_def [code]
-declare multiset_of.simps [code]
+declare mset.simps [code]
 
 
 fun fold_impl :: "('a \<Rightarrow> nat \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a \<times> nat) list \<Rightarrow> 'b"
diff -r 78a82c37b4b2 -r 484559628038 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu Jun 18 16:17:51 2015 +0200
+++ b/src/HOL/Library/Multiset.thy	Fri Jun 19 15:55:22 2015 +0200
@@ -963,46 +963,46 @@
 
 subsection \<open>Further conversions\<close>
 
-primrec multiset_of :: "'a list \<Rightarrow> 'a multiset" where
-  "multiset_of [] = {#}" |
-  "multiset_of (a # x) = multiset_of x + {# a #}"
+primrec mset :: "'a list \<Rightarrow> 'a multiset" where
+  "mset [] = {#}" |
+  "mset (a # x) = mset x + {# a #}"
 
 lemma in_multiset_in_set:
-  "x \<in># multiset_of xs \<longleftrightarrow> x \<in> set xs"
+  "x \<in># mset xs \<longleftrightarrow> x \<in> set xs"
   by (induct xs) simp_all
 
-lemma count_multiset_of:
-  "count (multiset_of xs) x = length (filter (\<lambda>y. x = y) xs)"
+lemma count_mset:
+  "count (mset xs) x = length (filter (\<lambda>y. x = y) xs)"
   by (induct xs) simp_all
 
-lemma multiset_of_zero_iff[simp]: "(multiset_of x = {#}) = (x = [])"
+lemma mset_zero_iff[simp]: "(mset x = {#}) = (x = [])"
   by (induct x) auto
 
-lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])"
+lemma mset_zero_iff_right[simp]: "({#} = mset x) = (x = [])"
 by (induct x) auto
 
-lemma set_mset_multiset_of[simp]: "set_mset (multiset_of x) = set x"
+lemma set_mset_mset[simp]: "set_mset (mset x) = set x"
 by (induct x) auto
 
-lemma mem_set_multiset_eq: "x \<in> set xs = (x :# multiset_of xs)"
+lemma mem_set_multiset_eq: "x \<in> set xs = (x :# mset xs)"
 by (induct xs) auto
 
-lemma size_multiset_of [simp]: "size (multiset_of xs) = length xs"
+lemma size_mset [simp]: "size (mset xs) = length xs"
   by (induct xs) simp_all
 
-lemma multiset_of_append [simp]:
-  "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys"
+lemma mset_append [simp]:
+  "mset (xs @ ys) = mset xs + mset ys"
   by (induct xs arbitrary: ys) (auto simp: ac_simps)
 
-lemma multiset_of_filter:
-  "multiset_of (filter P xs) = {#x :# multiset_of xs. P x #}"
+lemma mset_filter:
+  "mset (filter P xs) = {#x :# mset xs. P x #}"
   by (induct xs) simp_all
 
-lemma multiset_of_rev [simp]:
-  "multiset_of (rev xs) = multiset_of xs"
+lemma mset_rev [simp]:
+  "mset (rev xs) = mset xs"
   by (induct xs) simp_all
 
-lemma surj_multiset_of: "surj multiset_of"
+lemma surj_mset: "surj mset"
 apply (unfold surj_def)
 apply (rule allI)
 apply (rule_tac M = y in multiset_induct)
@@ -1011,72 +1011,72 @@
 apply auto
 done
 
-lemma set_count_greater_0: "set x = {a. count (multiset_of x) a > 0}"
+lemma set_count_greater_0: "set x = {a. count (mset x) a > 0}"
 by (induct x) auto
 
 lemma distinct_count_atmost_1:
-  "distinct x = (! a. count (multiset_of x) a = (if a \<in> set x then 1 else 0))"
+  "distinct x = (! a. count (mset x) a = (if a \<in> set x then 1 else 0))"
 apply (induct x, simp, rule iffI, simp_all)
 apply (rename_tac a b)
 apply (rule conjI)
-apply (simp_all add: set_mset_multiset_of [THEN sym] del: set_mset_multiset_of)
+apply (simp_all add: set_mset_mset [THEN sym] del: set_mset_mset)
 apply (erule_tac x = a in allE, simp, clarify)
 apply (erule_tac x = aa in allE, simp)
 done
 
-lemma multiset_of_eq_setD:
-  "multiset_of xs = multiset_of ys \<Longrightarrow> set xs = set ys"
+lemma mset_eq_setD:
+  "mset xs = mset ys \<Longrightarrow> set xs = set ys"
 by (rule) (auto simp add:multiset_eq_iff set_count_greater_0)
 
-lemma set_eq_iff_multiset_of_eq_distinct:
+lemma set_eq_iff_mset_eq_distinct:
   "distinct x \<Longrightarrow> distinct y \<Longrightarrow>
-    (set x = set y) = (multiset_of x = multiset_of y)"
+    (set x = set y) = (mset x = mset y)"
 by (auto simp: multiset_eq_iff distinct_count_atmost_1)
 
-lemma set_eq_iff_multiset_of_remdups_eq:
-   "(set x = set y) = (multiset_of (remdups x) = multiset_of (remdups y))"
+lemma set_eq_iff_mset_remdups_eq:
+   "(set x = set y) = (mset (remdups x) = mset (remdups y))"
 apply (rule iffI)
-apply (simp add: set_eq_iff_multiset_of_eq_distinct[THEN iffD1])
+apply (simp add: set_eq_iff_mset_eq_distinct[THEN iffD1])
 apply (drule distinct_remdups [THEN distinct_remdups
-      [THEN set_eq_iff_multiset_of_eq_distinct [THEN iffD2]]])
+      [THEN set_eq_iff_mset_eq_distinct [THEN iffD2]]])
 apply simp
 done
 
-lemma multiset_of_compl_union [simp]:
-  "multiset_of [x\<leftarrow>xs. P x] + multiset_of [x\<leftarrow>xs. \<not>P x] = multiset_of xs"
+lemma mset_compl_union [simp]:
+  "mset [x\<leftarrow>xs. P x] + mset [x\<leftarrow>xs. \<not>P x] = mset xs"
   by (induct xs) (auto simp: ac_simps)
 
-lemma nth_mem_multiset_of: "i < length ls \<Longrightarrow> (ls ! i) :# multiset_of ls"
+lemma nth_mem_mset: "i < length ls \<Longrightarrow> (ls ! i) :# mset ls"
 apply (induct ls arbitrary: i)
  apply simp
 apply (case_tac i)
  apply auto
 done
 
-lemma multiset_of_remove1[simp]:
-  "multiset_of (remove1 a xs) = multiset_of xs - {#a#}"
+lemma mset_remove1[simp]:
+  "mset (remove1 a xs) = mset xs - {#a#}"
 by (induct xs) (auto simp add: multiset_eq_iff)
 
-lemma multiset_of_eq_length:
-  assumes "multiset_of xs = multiset_of ys"
+lemma mset_eq_length:
+  assumes "mset xs = mset ys"
   shows "length xs = length ys"
-  using assms by (metis size_multiset_of)
-
-lemma multiset_of_eq_length_filter:
-  assumes "multiset_of xs = multiset_of ys"
+  using assms by (metis size_mset)
+
+lemma mset_eq_length_filter:
+  assumes "mset xs = mset ys"
   shows "length (filter (\<lambda>x. z = x) xs) = length (filter (\<lambda>y. z = y) ys)"
-  using assms by (metis count_multiset_of)
+  using assms by (metis count_mset)
 
 lemma fold_multiset_equiv:
   assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
-    and equiv: "multiset_of xs = multiset_of ys"
+    and equiv: "mset xs = mset ys"
   shows "List.fold f xs = List.fold f ys"
 using f equiv [symmetric]
 proof (induct xs arbitrary: ys)
   case Nil then show ?case by simp
 next
   case (Cons x xs)
-  then have *: "set ys = set (x # xs)" by (blast dest: multiset_of_eq_setD)
+  then have *: "set ys = set (x # xs)" by (blast dest: mset_eq_setD)
   have "\<And>x y. x \<in> set ys \<Longrightarrow> y \<in> set ys \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
     by (rule Cons.prems(1)) (simp_all add: *)
   moreover from * have "x \<in> set ys" by simp
@@ -1085,12 +1085,12 @@
   ultimately show ?case by simp
 qed
 
-lemma multiset_of_insort [simp]:
-  "multiset_of (insort x xs) = multiset_of xs + {#x#}"
+lemma mset_insort [simp]:
+  "mset (insort x xs) = mset xs + {#x#}"
   by (induct xs) (simp_all add: ac_simps)
 
-lemma multiset_of_map:
-  "multiset_of (map f xs) = image_mset f (multiset_of xs)"
+lemma mset_map:
+  "mset (map f xs) = image_mset f (mset xs)"
   by (induct xs) simp_all
 
 definition mset_set :: "'a set \<Rightarrow> 'a multiset"
@@ -1154,12 +1154,12 @@
 
 end
 
-lemma multiset_of_sorted_list_of_multiset [simp]:
-  "multiset_of (sorted_list_of_multiset M) = M"
+lemma mset_sorted_list_of_multiset [simp]:
+  "mset (sorted_list_of_multiset M) = M"
 by (induct M) simp_all
 
-lemma sorted_list_of_multiset_multiset_of [simp]:
-  "sorted_list_of_multiset (multiset_of xs) = sort xs"
+lemma sorted_list_of_multiset_mset [simp]:
+  "sorted_list_of_multiset (mset xs) = sort xs"
 by (induct xs) simp_all
 
 lemma finite_set_mset_mset_set[simp]:
@@ -1386,12 +1386,12 @@
 context linorder
 begin
 
-lemma multiset_of_insort [simp]:
-  "multiset_of (insort_key k x xs) = {#x#} + multiset_of xs"
+lemma mset_insort [simp]:
+  "mset (insort_key k x xs) = {#x#} + mset xs"
   by (induct xs) (simp_all add: ac_simps)
 
-lemma multiset_of_sort [simp]:
-  "multiset_of (sort_key k xs) = multiset_of xs"
+lemma mset_sort [simp]:
+  "mset (sort_key k xs) = mset xs"
   by (induct xs) (simp_all add: ac_simps)
 
 text \<open>
@@ -1400,7 +1400,7 @@
 \<close>
 
 lemma properties_for_sort_key:
-  assumes "multiset_of ys = multiset_of xs"
+  assumes "mset ys = mset xs"
   and "\<And>k. k \<in> set ys \<Longrightarrow> filter (\<lambda>x. f k = f x) ys = filter (\<lambda>x. f k = f x) xs"
   and "sorted (map f ys)"
   shows "sort_key f xs = ys"
@@ -1420,14 +1420,14 @@
 qed
 
 lemma properties_for_sort:
-  assumes multiset: "multiset_of ys = multiset_of xs"
+  assumes multiset: "mset ys = mset xs"
   and "sorted ys"
   shows "sort xs = ys"
 proof (rule properties_for_sort_key)
-  from multiset show "multiset_of ys = multiset_of xs" .
+  from multiset show "mset ys = mset xs" .
   from \<open>sorted ys\<close> show "sorted (map (\<lambda>x. x) ys)" by simp
   from multiset have "\<And>k. length (filter (\<lambda>y. k = y) ys) = length (filter (\<lambda>x. k = x) xs)"
-    by (rule multiset_of_eq_length_filter)
+    by (rule mset_eq_length_filter)
   then have "\<And>k. replicate (length (filter (\<lambda>y. k = y) ys)) k = replicate (length (filter (\<lambda>x. k = x) xs)) k"
     by simp
   then show "\<And>k. k \<in> set ys \<Longrightarrow> filter (\<lambda>y. k = y) ys = filter (\<lambda>x. k = x) xs"
@@ -1439,8 +1439,8 @@
     @ [x\<leftarrow>xs. f x = f (xs ! (length xs div 2))]
     @ sort_key f [x\<leftarrow>xs. f x > f (xs ! (length xs div 2))]" (is "sort_key f ?lhs = ?rhs")
 proof (rule properties_for_sort_key)
-  show "multiset_of ?rhs = multiset_of ?lhs"
-    by (rule multiset_eqI) (auto simp add: multiset_of_filter)
+  show "mset ?rhs = mset ?lhs"
+    by (rule multiset_eqI) (auto simp add: mset_filter)
 next
   show "sorted (map f ?rhs)"
     by (auto simp add: sorted_append intro: sorted_map_same)
@@ -1523,11 +1523,11 @@
 
 hide_const (open) part
 
-lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le># multiset_of xs"
+lemma mset_remdups_le: "mset (remdups xs) \<le># mset xs"
   by (induct xs) (auto intro: subset_mset.order_trans)
 
-lemma multiset_of_update:
-  "i < length ls \<Longrightarrow> multiset_of (ls[i := v]) = multiset_of ls - {#ls ! i#} + {#v#}"
+lemma mset_update:
+  "i < length ls \<Longrightarrow> mset (ls[i := v]) = mset ls - {#ls ! i#} + {#v#}"
 proof (induct ls arbitrary: i)
   case Nil then show ?case by simp
 next
@@ -1544,15 +1544,15 @@
       apply (subst add.assoc [symmetric])
       apply simp
       apply (rule mset_le_multiset_union_diff_commute)
-      apply (simp add: mset_le_single nth_mem_multiset_of)
+      apply (simp add: mset_le_single nth_mem_mset)
       done
   qed
 qed
 
-lemma multiset_of_swap:
+lemma mset_swap:
   "i < length ls \<Longrightarrow> j < length ls \<Longrightarrow>
-    multiset_of (ls[j := ls ! i, i := ls ! j]) = multiset_of ls"
-  by (cases "i = j") (simp_all add: multiset_of_update nth_mem_multiset_of)
+    mset (ls[j := ls ! i, i := ls ! j]) = mset ls"
+  by (cases "i = j") (simp_all add: mset_update nth_mem_mset)
 
 
 subsection \<open>The multiset order\<close>
@@ -2071,51 +2071,51 @@
 
 subsection \<open>Naive implementation using lists\<close>
 
-code_datatype multiset_of
+code_datatype mset
 
 lemma [code]:
-  "{#} = multiset_of []"
+  "{#} = mset []"
   by simp
 
 lemma [code]:
-  "{#x#} = multiset_of [x]"
+  "{#x#} = mset [x]"
   by simp
 
 lemma union_code [code]:
-  "multiset_of xs + multiset_of ys = multiset_of (xs @ ys)"
+  "mset xs + mset ys = mset (xs @ ys)"
   by simp
 
 lemma [code]:
-  "image_mset f (multiset_of xs) = multiset_of (map f xs)"
-  by (simp add: multiset_of_map)
+  "image_mset f (mset xs) = mset (map f xs)"
+  by (simp add: mset_map)
 
 lemma [code]:
-  "filter_mset f (multiset_of xs) = multiset_of (filter f xs)"
-  by (simp add: multiset_of_filter)
+  "filter_mset f (mset xs) = mset (filter f xs)"
+  by (simp add: mset_filter)
 
 lemma [code]:
-  "multiset_of xs - multiset_of ys = multiset_of (fold remove1 ys xs)"
+  "mset xs - mset ys = mset (fold remove1 ys xs)"
   by (rule sym, induct ys arbitrary: xs) (simp_all add: diff_add diff_right_commute)
 
 lemma [code]:
-  "multiset_of xs #\<inter> multiset_of ys =
-    multiset_of (snd (fold (\<lambda>x (ys, zs).
+  "mset xs #\<inter> mset ys =
+    mset (snd (fold (\<lambda>x (ys, zs).
       if x \<in> set ys then (remove1 x ys, x # zs) else (ys, zs)) xs (ys, [])))"
 proof -
-  have "\<And>zs. multiset_of (snd (fold (\<lambda>x (ys, zs).
+  have "\<And>zs. mset (snd (fold (\<lambda>x (ys, zs).
     if x \<in> set ys then (remove1 x ys, x # zs) else (ys, zs)) xs (ys, zs))) =
-      (multiset_of xs #\<inter> multiset_of ys) + multiset_of zs"
+      (mset xs #\<inter> mset ys) + mset zs"
     by (induct xs arbitrary: ys)
       (auto simp add: mem_set_multiset_eq inter_add_right1 inter_add_right2 ac_simps)
   then show ?thesis by simp
 qed
 
 lemma [code]:
-  "multiset_of xs #\<union> multiset_of ys =
-    multiset_of (split append (fold (\<lambda>x (ys, zs). (remove1 x ys, x # zs)) xs (ys, [])))"
+  "mset xs #\<union> mset ys =
+    mset (split append (fold (\<lambda>x (ys, zs). (remove1 x ys, x # zs)) xs (ys, [])))"
 proof -
-  have "\<And>zs. multiset_of (split append (fold (\<lambda>x (ys, zs). (remove1 x ys, x # zs)) xs (ys, zs))) =
-      (multiset_of xs #\<union> multiset_of ys) + multiset_of zs"
+  have "\<And>zs. mset (split append (fold (\<lambda>x (ys, zs). (remove1 x ys, x # zs)) xs (ys, zs))) =
+      (mset xs #\<union> mset ys) + mset zs"
     by (induct xs arbitrary: ys) (simp_all add: multiset_eq_iff)
   then show ?thesis by simp
 qed
@@ -2123,26 +2123,26 @@
 declare in_multiset_in_set [code_unfold]
 
 lemma [code]:
-  "count (multiset_of xs) x = fold (\<lambda>y. if x = y then Suc else id) xs 0"
+  "count (mset xs) x = fold (\<lambda>y. if x = y then Suc else id) xs 0"
 proof -
-  have "\<And>n. fold (\<lambda>y. if x = y then Suc else id) xs n = count (multiset_of xs) x + n"
+  have "\<And>n. fold (\<lambda>y. if x = y then Suc else id) xs n = count (mset xs) x + n"
     by (induct xs) simp_all
   then show ?thesis by simp
 qed
 
-declare set_mset_multiset_of [code]
-
-declare sorted_list_of_multiset_multiset_of [code]
+declare set_mset_mset [code]
+
+declare sorted_list_of_multiset_mset [code]
 
 lemma [code]: -- \<open>not very efficient, but representation-ignorant!\<close>
-  "mset_set A = multiset_of (sorted_list_of_set A)"
+  "mset_set A = mset (sorted_list_of_set A)"
   apply (cases "finite A")
   apply simp_all
   apply (induct A rule: finite_induct)
   apply (simp_all add: add.commute)
   done
 
-declare size_multiset_of [code]
+declare size_mset [code]
 
 fun ms_lesseq_impl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool option" where
   "ms_lesseq_impl [] ys = Some (ys \<noteq> [])"
@@ -2150,9 +2150,9 @@
      None \<Rightarrow> None
    | Some (ys1,_,ys2) \<Rightarrow> ms_lesseq_impl xs (ys1 @ ys2))"
 
-lemma ms_lesseq_impl: "(ms_lesseq_impl xs ys = None \<longleftrightarrow> \<not> multiset_of xs \<le># multiset_of ys) \<and>
-  (ms_lesseq_impl xs ys = Some True \<longleftrightarrow> multiset_of xs <# multiset_of ys) \<and>
-  (ms_lesseq_impl xs ys = Some False \<longrightarrow> multiset_of xs = multiset_of ys)"
+lemma ms_lesseq_impl: "(ms_lesseq_impl xs ys = None \<longleftrightarrow> \<not> mset xs \<le># mset ys) \<and>
+  (ms_lesseq_impl xs ys = Some True \<longleftrightarrow> mset xs <# mset ys) \<and>
+  (ms_lesseq_impl xs ys = Some False \<longrightarrow> mset xs = mset ys)"
 proof (induct xs arbitrary: ys)
   case (Nil ys)
   show ?case by (auto simp: mset_less_empty_nonempty)
@@ -2163,13 +2163,13 @@
     case None
     hence x: "x \<notin> set ys" by (simp add: extract_None_iff)
     {
-      assume "multiset_of (x # xs) \<le># multiset_of ys"
+      assume "mset (x # xs) \<le># mset ys"
       from set_mset_mono[OF this] x have False by simp
     } note nle = this
     moreover
     {
-      assume "multiset_of (x # xs) <# multiset_of ys"
-      hence "multiset_of (x # xs) \<le># multiset_of ys" by auto
+      assume "mset (x # xs) <# mset ys"
+      hence "mset (x # xs) \<le># mset ys" by auto
       from nle[OF this] have False .
     }
     ultimately show ?thesis using None by auto
@@ -2178,7 +2178,7 @@
     obtain ys1 y ys2 where res: "res = (ys1,y,ys2)" by (cases res, auto)
     note Some = Some[unfolded res]
     from extract_SomeE[OF Some] have "ys = ys1 @ x # ys2" by simp
-    hence id: "multiset_of ys = multiset_of (ys1 @ ys2) + {#x#}"
+    hence id: "mset ys = mset (ys1 @ ys2) + {#x#}"
       by (auto simp: ac_simps)
     show ?thesis unfolding ms_lesseq_impl.simps
       unfolding Some option.simps split
@@ -2188,10 +2188,10 @@
   qed
 qed
 
-lemma [code]: "multiset_of xs \<le># multiset_of ys \<longleftrightarrow> ms_lesseq_impl xs ys \<noteq> None"
+lemma [code]: "mset xs \<le># mset ys \<longleftrightarrow> ms_lesseq_impl xs ys \<noteq> None"
   using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
 
-lemma [code]: "multiset_of xs <# multiset_of ys \<longleftrightarrow> ms_lesseq_impl xs ys = Some True"
+lemma [code]: "mset xs <# mset ys \<longleftrightarrow> ms_lesseq_impl xs ys = Some True"
   using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
 
 instantiation multiset :: (equal) equal
@@ -2199,7 +2199,7 @@
 
 definition
   [code del]: "HOL.equal A (B :: 'a multiset) \<longleftrightarrow> A = B"
-lemma [code]: "HOL.equal (multiset_of xs) (multiset_of ys) \<longleftrightarrow> ms_lesseq_impl xs ys = Some False"
+lemma [code]: "HOL.equal (mset xs) (mset ys) \<longleftrightarrow> ms_lesseq_impl xs ys = Some False"
   unfolding equal_multiset_def
   using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
 
@@ -2208,13 +2208,13 @@
 end
 
 lemma [code]:
-  "msetsum (multiset_of xs) = listsum xs"
+  "msetsum (mset xs) = listsum xs"
   by (induct xs) (simp_all add: add.commute)
 
 lemma [code]:
-  "msetprod (multiset_of xs) = fold times xs 1"
+  "msetprod (mset xs) = fold times xs 1"
 proof -
-  have "\<And>x. fold times xs x = msetprod (multiset_of xs) * x"
+  have "\<And>x. fold times xs x = msetprod (mset xs) * x"
     by (induct xs) (simp_all add: mult.assoc)
   then show ?thesis by simp
 qed
@@ -2229,7 +2229,7 @@
 definition (in term_syntax)
   msetify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
     \<Rightarrow> 'a multiset \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
-  [code_unfold]: "msetify xs = Code_Evaluation.valtermify multiset_of {\<cdot>} xs"
+  [code_unfold]: "msetify xs = Code_Evaluation.valtermify mset {\<cdot>} xs"
 
 notation fcomp (infixl "\<circ>>" 60)
 notation scomp (infixl "\<circ>\<rightarrow>" 60)
@@ -2264,12 +2264,12 @@
 subsection \<open>BNF setup\<close>
 
 definition rel_mset where
-  "rel_mset R X Y \<longleftrightarrow> (\<exists>xs ys. multiset_of xs = X \<and> multiset_of ys = Y \<and> list_all2 R xs ys)"
-
-lemma multiset_of_zip_take_Cons_drop_twice:
+  "rel_mset R X Y \<longleftrightarrow> (\<exists>xs ys. mset xs = X \<and> mset ys = Y \<and> list_all2 R xs ys)"
+
+lemma mset_zip_take_Cons_drop_twice:
   assumes "length xs = length ys" "j \<le> length xs"
-  shows "multiset_of (zip (take j xs @ x # drop j xs) (take j ys @ y # drop j ys)) =
-    multiset_of (zip xs ys) + {#(x, y)#}"
+  shows "mset (zip (take j xs @ x # drop j xs) (take j ys @ y # drop j ys)) =
+    mset (zip xs ys) + {#(x, y)#}"
 using assms
 proof (induct xs ys arbitrary: x y j rule: list_induct2)
   case Nil
@@ -2288,17 +2288,17 @@
       by (case_tac j) simp
     hence "k \<le> length xs"
       using Cons.prems by auto
-    hence "multiset_of (zip (take k xs @ x # drop k xs) (take k ys @ y # drop k ys)) =
-      multiset_of (zip xs ys) + {#(x, y)#}"
+    hence "mset (zip (take k xs @ x # drop k xs) (take k ys @ y # drop k ys)) =
+      mset (zip xs ys) + {#(x, y)#}"
       by (rule Cons.hyps(2))
     thus ?thesis
       unfolding k by (auto simp: add.commute union_lcomm)
   qed
 qed
 
-lemma ex_multiset_of_zip_left:
-  assumes "length xs = length ys" "multiset_of xs' = multiset_of xs"
-  shows "\<exists>ys'. length ys' = length xs' \<and> multiset_of (zip xs' ys') = multiset_of (zip xs ys)"
+lemma ex_mset_zip_left:
+  assumes "length xs = length ys" "mset xs' = mset xs"
+  shows "\<exists>ys'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip xs ys)"
 using assms
 proof (induct xs ys arbitrary: xs' rule: list_induct2)
   case Nil
@@ -2307,57 +2307,57 @@
 next
   case (Cons x xs y ys xs')
   obtain j where j_len: "j < length xs'" and nth_j: "xs' ! j = x"
-    by (metis Cons.prems in_set_conv_nth list.set_intros(1) multiset_of_eq_setD)
+    by (metis Cons.prems in_set_conv_nth list.set_intros(1) mset_eq_setD)
 
   def xsa \<equiv> "take j xs' @ drop (Suc j) xs'"
-  have "multiset_of xs' = {#x#} + multiset_of xsa"
+  have "mset xs' = {#x#} + mset xsa"
     unfolding xsa_def using j_len nth_j
     by (metis (no_types) ab_semigroup_add_class.add_ac(1) append_take_drop_id Cons_nth_drop_Suc
-      multiset_of.simps(2) union_code add.commute)
-  hence ms_x: "multiset_of xsa = multiset_of xs"
-    by (metis Cons.prems add.commute add_right_imp_eq multiset_of.simps(2))
+      mset.simps(2) union_code add.commute)
+  hence ms_x: "mset xsa = mset xs"
+    by (metis Cons.prems add.commute add_right_imp_eq mset.simps(2))
   then obtain ysa where
-    len_a: "length ysa = length xsa" and ms_a: "multiset_of (zip xsa ysa) = multiset_of (zip xs ys)"
+    len_a: "length ysa = length xsa" and ms_a: "mset (zip xsa ysa) = mset (zip xs ys)"
     using Cons.hyps(2) by blast
 
   def ys' \<equiv> "take j ysa @ y # drop j ysa"
   have xs': "xs' = take j xsa @ x # drop j xsa"
     using ms_x j_len nth_j Cons.prems xsa_def
     by (metis append_eq_append_conv append_take_drop_id diff_Suc_Suc Cons_nth_drop_Suc length_Cons
-      length_drop size_multiset_of)
+      length_drop size_mset)
   have j_len': "j \<le> length xsa"
     using j_len xs' xsa_def
     by (metis add_Suc_right append_take_drop_id length_Cons length_append less_eq_Suc_le not_less)
   have "length ys' = length xs'"
     unfolding ys'_def using Cons.prems len_a ms_x
-    by (metis add_Suc_right append_take_drop_id length_Cons length_append multiset_of_eq_length)
-  moreover have "multiset_of (zip xs' ys') = multiset_of (zip (x # xs) (y # ys))"
+    by (metis add_Suc_right append_take_drop_id length_Cons length_append mset_eq_length)
+  moreover have "mset (zip xs' ys') = mset (zip (x # xs) (y # ys))"
     unfolding xs' ys'_def
-    by (rule trans[OF multiset_of_zip_take_Cons_drop_twice])
+    by (rule trans[OF mset_zip_take_Cons_drop_twice])
       (auto simp: len_a ms_a j_len' add.commute)
   ultimately show ?case
     by blast
 qed
 
 lemma list_all2_reorder_left_invariance:
-  assumes rel: "list_all2 R xs ys" and ms_x: "multiset_of xs' = multiset_of xs"
-  shows "\<exists>ys'. list_all2 R xs' ys' \<and> multiset_of ys' = multiset_of ys"
+  assumes rel: "list_all2 R xs ys" and ms_x: "mset xs' = mset xs"
+  shows "\<exists>ys'. list_all2 R xs' ys' \<and> mset ys' = mset ys"
 proof -
   have len: "length xs = length ys"
     using rel list_all2_conv_all_nth by auto
   obtain ys' where
-    len': "length xs' = length ys'" and ms_xy: "multiset_of (zip xs' ys') = multiset_of (zip xs ys)"
-    using len ms_x by (metis ex_multiset_of_zip_left)
+    len': "length xs' = length ys'" and ms_xy: "mset (zip xs' ys') = mset (zip xs ys)"
+    using len ms_x by (metis ex_mset_zip_left)
   have "list_all2 R xs' ys'"
-    using assms(1) len' ms_xy unfolding list_all2_iff by (blast dest: multiset_of_eq_setD)
-  moreover have "multiset_of ys' = multiset_of ys"
-    using len len' ms_xy map_snd_zip multiset_of_map by metis
+    using assms(1) len' ms_xy unfolding list_all2_iff by (blast dest: mset_eq_setD)
+  moreover have "mset ys' = mset ys"
+    using len len' ms_xy map_snd_zip mset_map by metis
   ultimately show ?thesis
     by blast
 qed
 
-lemma ex_multiset_of: "\<exists>xs. multiset_of xs = X"
-  by (induct X) (simp, metis multiset_of.simps(2))
+lemma ex_mset: "\<exists>xs. mset xs = X"
+  by (induct X) (simp, metis mset.simps(2))
 
 bnf "'a multiset"
   map: image_mset
@@ -2403,19 +2403,19 @@
     unfolding rel_mset_def[abs_def] BNF_Def.Grp_def OO_def
     apply (rule ext)+
     apply auto
-     apply (rule_tac x = "multiset_of (zip xs ys)" in exI; auto)
-        apply (metis list_all2_lengthD map_fst_zip multiset_of_map)
+     apply (rule_tac x = "mset (zip xs ys)" in exI; auto)
+        apply (metis list_all2_lengthD map_fst_zip mset_map)
        apply (auto simp: list_all2_iff)[1]
-      apply (metis list_all2_lengthD map_snd_zip multiset_of_map)
+      apply (metis list_all2_lengthD map_snd_zip mset_map)
      apply (auto simp: list_all2_iff)[1]
     apply (rename_tac XY)
-    apply (cut_tac X = XY in ex_multiset_of)
+    apply (cut_tac X = XY in ex_mset)
     apply (erule exE)
     apply (rename_tac xys)
     apply (rule_tac x = "map fst xys" in exI)
-    apply (auto simp: multiset_of_map)
+    apply (auto simp: mset_map)
     apply (rule_tac x = "map snd xys" in exI)
-    apply (auto simp: multiset_of_map list_all2I subset_eq zip_map_fst_snd)
+    apply (auto simp: mset_map list_all2I subset_eq zip_map_fst_snd)
     done
 next
   show "\<And>z. z \<in> set_mset {#} \<Longrightarrow> False"
diff -r 78a82c37b4b2 -r 484559628038 src/HOL/Library/Permutation.thy
--- a/src/HOL/Library/Permutation.thy	Thu Jun 18 16:17:51 2015 +0200
+++ b/src/HOL/Library/Permutation.thy	Fri Jun 19 15:55:22 2015 +0200
@@ -120,7 +120,7 @@
   apply (blast intro: perm_append_swap)
   done
 
-lemma multiset_of_eq_perm: "multiset_of xs = multiset_of ys \<longleftrightarrow> xs <~~> ys"
+lemma mset_eq_perm: "mset xs = mset ys \<longleftrightarrow> xs <~~> ys"
   apply (rule iffI)
   apply (erule_tac [2] perm.induct)
   apply (simp_all add: union_ac)
@@ -140,15 +140,15 @@
   apply simp
   done
 
-lemma multiset_of_le_perm_append: "multiset_of xs \<le># multiset_of ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
-  apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv)
-  apply (insert surj_multiset_of)
+lemma mset_le_perm_append: "mset xs \<le># mset ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
+  apply (auto simp: mset_eq_perm[THEN sym] mset_le_exists_conv)
+  apply (insert surj_mset)
   apply (drule surjD)
   apply (blast intro: sym)+
   done
 
 lemma perm_set_eq: "xs <~~> ys \<Longrightarrow> set xs = set ys"
-  by (metis multiset_of_eq_perm multiset_of_eq_setD)
+  by (metis mset_eq_perm mset_eq_setD)
 
 lemma perm_distinct_iff: "xs <~~> ys \<Longrightarrow> distinct xs = distinct ys"
   apply (induct pred: perm)
diff -r 78a82c37b4b2 -r 484559628038 src/HOL/Library/Tree_Multiset.thy
--- a/src/HOL/Library/Tree_Multiset.thy	Thu Jun 18 16:17:51 2015 +0200
+++ b/src/HOL/Library/Tree_Multiset.thy	Fri Jun 19 15:55:22 2015 +0200
@@ -26,10 +26,10 @@
 lemma mset_iff_set_tree: "x \<in># mset_tree t \<longleftrightarrow> x \<in> set_tree t"
 by(induction t arbitrary: x) auto
 
-lemma multiset_of_preorder[simp]: "multiset_of (preorder t) = mset_tree t"
+lemma mset_preorder[simp]: "mset (preorder t) = mset_tree t"
 by (induction t) (auto simp: ac_simps)
 
-lemma multiset_of_inorder[simp]: "multiset_of (inorder t) = mset_tree t"
+lemma mset_inorder[simp]: "mset (inorder t) = mset_tree t"
 by (induction t) (auto simp: ac_simps)
 
 lemma map_mirror: "mset_tree (mirror t) = mset_tree t"
diff -r 78a82c37b4b2 -r 484559628038 src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Thu Jun 18 16:17:51 2015 +0200
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Fri Jun 19 15:55:22 2015 +0200
@@ -239,9 +239,9 @@
   assumes "t xs = t ys"
   shows "\<exists>f. bij_betw f {..<length xs} {..<length ys} \<and> (\<forall>i<length xs. xs ! i = ys ! (f i))"
 proof -
-  have "count (multiset_of xs) = count (multiset_of ys)"
-    using assms by (simp add: fun_eq_iff count_multiset_of t_def)
-  then have "xs <~~> ys" unfolding multiset_of_eq_perm count_inject .
+  have "count (mset xs) = count (mset ys)"
+    using assms by (simp add: fun_eq_iff count_mset t_def)
+  then have "xs <~~> ys" unfolding mset_eq_perm count_inject .
   then show ?thesis by (rule permutation_Ex_bij)
 qed
 
diff -r 78a82c37b4b2 -r 484559628038 src/HOL/Proofs/Extraction/Euclid.thy
--- a/src/HOL/Proofs/Extraction/Euclid.thy	Thu Jun 18 16:17:51 2015 +0200
+++ b/src/HOL/Proofs/Extraction/Euclid.thy	Fri Jun 19 15:55:22 2015 +0200
@@ -123,7 +123,7 @@
   qed
 qed
 
-lemma dvd_prod [iff]: "n dvd (PROD m\<Colon>nat:#multiset_of (n # ns). m)"
+lemma dvd_prod [iff]: "n dvd (PROD m\<Colon>nat:#mset (n # ns). m)"
   by (simp add: msetprod_Un msetprod_singleton)
 
 definition all_prime :: "nat list \<Rightarrow> bool" where
@@ -140,13 +140,13 @@
 
 lemma split_all_prime:
   assumes "all_prime ms" and "all_prime ns"
-  shows "\<exists>qs. all_prime qs \<and> (PROD m\<Colon>nat:#multiset_of qs. m) =
-    (PROD m\<Colon>nat:#multiset_of ms. m) * (PROD m\<Colon>nat:#multiset_of ns. m)" (is "\<exists>qs. ?P qs \<and> ?Q qs")
+  shows "\<exists>qs. all_prime qs \<and> (PROD m\<Colon>nat:#mset qs. m) =
+    (PROD m\<Colon>nat:#mset ms. m) * (PROD m\<Colon>nat:#mset ns. m)" (is "\<exists>qs. ?P qs \<and> ?Q qs")
 proof -
   from assms have "all_prime (ms @ ns)"
     by (simp add: all_prime_append)
-  moreover from assms have "(PROD m\<Colon>nat:#multiset_of (ms @ ns). m) =
-    (PROD m\<Colon>nat:#multiset_of ms. m) * (PROD m\<Colon>nat:#multiset_of ns. m)"
+  moreover from assms have "(PROD m\<Colon>nat:#mset (ms @ ns). m) =
+    (PROD m\<Colon>nat:#mset ms. m) * (PROD m\<Colon>nat:#mset ns. m)"
     by (simp add: msetprod_Un)
   ultimately have "?P (ms @ ns) \<and> ?Q (ms @ ns)" ..
   then show ?thesis ..
@@ -154,11 +154,11 @@
 
 lemma all_prime_nempty_g_one:
   assumes "all_prime ps" and "ps \<noteq> []"
-  shows "Suc 0 < (PROD m\<Colon>nat:#multiset_of ps. m)"
+  shows "Suc 0 < (PROD m\<Colon>nat:#mset ps. m)"
   using `ps \<noteq> []` `all_prime ps` unfolding One_nat_def [symmetric] by (induct ps rule: list_nonempty_induct)
     (simp_all add: all_prime_simps msetprod_singleton msetprod_Un prime_gt_1_nat less_1_mult del: One_nat_def)
 
-lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#multiset_of ps. m) = n)"
+lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#mset ps. m) = n)"
 proof (induct n rule: nat_wf_ind)
   case (1 n)
   from `Suc 0 < n`
@@ -169,21 +169,21 @@
     assume "\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k"
     then obtain m k where m: "Suc 0 < m" and k: "Suc 0 < k" and mn: "m < n"
       and kn: "k < n" and nmk: "n = m * k" by iprover
-    from mn and m have "\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#multiset_of ps. m) = m" by (rule 1)
-    then obtain ps1 where "all_prime ps1" and prod_ps1_m: "(PROD m\<Colon>nat:#multiset_of ps1. m) = m"
+    from mn and m have "\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#mset ps. m) = m" by (rule 1)
+    then obtain ps1 where "all_prime ps1" and prod_ps1_m: "(PROD m\<Colon>nat:#mset ps1. m) = m"
       by iprover
-    from kn and k have "\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#multiset_of ps. m) = k" by (rule 1)
-    then obtain ps2 where "all_prime ps2" and prod_ps2_k: "(PROD m\<Colon>nat:#multiset_of ps2. m) = k"
+    from kn and k have "\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#mset ps. m) = k" by (rule 1)
+    then obtain ps2 where "all_prime ps2" and prod_ps2_k: "(PROD m\<Colon>nat:#mset ps2. m) = k"
       by iprover
     from `all_prime ps1` `all_prime ps2`
-    have "\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#multiset_of ps. m) =
-      (PROD m\<Colon>nat:#multiset_of ps1. m) * (PROD m\<Colon>nat:#multiset_of ps2. m)"
+    have "\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#mset ps. m) =
+      (PROD m\<Colon>nat:#mset ps1. m) * (PROD m\<Colon>nat:#mset ps2. m)"
       by (rule split_all_prime)
     with prod_ps1_m prod_ps2_k nmk show ?thesis by simp
   next
     assume "prime n" then have "all_prime [n]" by (simp add: all_prime_simps)
-    moreover have "(PROD m\<Colon>nat:#multiset_of [n]. m) = n" by (simp add: msetprod_singleton)
-    ultimately have "all_prime [n] \<and> (PROD m\<Colon>nat:#multiset_of [n]. m) = n" ..
+    moreover have "(PROD m\<Colon>nat:#mset [n]. m) = n" by (simp add: msetprod_singleton)
+    ultimately have "all_prime [n] \<and> (PROD m\<Colon>nat:#mset [n]. m) = n" ..
     then show ?thesis ..
   qed
 qed
@@ -193,7 +193,7 @@
   shows "\<exists>p. prime p \<and> p dvd n"
 proof -
   from N obtain ps where "all_prime ps"
-    and prod_ps: "n = (PROD m\<Colon>nat:#multiset_of ps. m)" using factor_exists
+    and prod_ps: "n = (PROD m\<Colon>nat:#mset ps. m)" using factor_exists
     by simp iprover
   with N have "ps \<noteq> []"
     by (auto simp add: all_prime_nempty_g_one msetprod_empty)
diff -r 78a82c37b4b2 -r 484559628038 src/HOL/Quotient_Examples/FSet.thy
--- a/src/HOL/Quotient_Examples/FSet.thy	Thu Jun 18 16:17:51 2015 +0200
+++ b/src/HOL/Quotient_Examples/FSet.thy	Fri Jun 19 15:55:22 2015 +0200
@@ -338,8 +338,8 @@
   case True
   then have "\<And>x y. x \<in> set (remdups xs) \<Longrightarrow> y \<in> set (remdups xs) \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
     by (rule rsp_foldE)
-  moreover from assms have "multiset_of (remdups xs) = multiset_of (remdups ys)"
-    by (simp add: set_eq_iff_multiset_of_remdups_eq)
+  moreover from assms have "mset (remdups xs) = mset (remdups ys)"
+    by (simp add: set_eq_iff_mset_remdups_eq)
   ultimately have "fold f (remdups xs) = fold f (remdups ys)"
     by (rule fold_multiset_equiv)
   with True show ?thesis by (simp add: fold_once_fold_remdups)
diff -r 78a82c37b4b2 -r 484559628038 src/HOL/UNITY/Comp/AllocBase.thy
--- a/src/HOL/UNITY/Comp/AllocBase.thy	Thu Jun 18 16:17:51 2015 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy	Fri Jun 19 15:55:22 2015 +0200
@@ -17,7 +17,7 @@
   "tokens [] = 0"
 | "tokens (x#xs) = x + tokens xs"
 
-abbreviation (input) "bag_of \<equiv> multiset_of"
+abbreviation (input) "bag_of \<equiv> mset"
 
 lemma setsum_fun_mono [rule_format]:
      "!!f :: nat=>nat.  
diff -r 78a82c37b4b2 -r 484559628038 src/HOL/ZF/LProd.thy
--- a/src/HOL/ZF/LProd.thy	Thu Jun 18 16:17:51 2015 +0200
+++ b/src/HOL/ZF/LProd.thy	Fri Jun 19 15:55:22 2015 +0200
@@ -34,7 +34,7 @@
 lemma lprod_subset: "S \<subseteq> R \<Longrightarrow> lprod S \<subseteq> lprod R"
   by (auto intro: lprod_subset_elem)
 
-lemma lprod_implies_mult: "(as, bs) \<in> lprod R \<Longrightarrow> trans R \<Longrightarrow> (multiset_of as, multiset_of bs) \<in> mult R"
+lemma lprod_implies_mult: "(as, bs) \<in> lprod R \<Longrightarrow> trans R \<Longrightarrow> (mset as, mset bs) \<in> mult R"
 proof (induct as bs rule: lprod.induct)
   case (lprod_single a b)
   note step = one_step_implies_mult[
@@ -43,9 +43,9 @@
 next
   case (lprod_list ah at bh bt a b)
   then have transR: "trans R" by auto
-  have as: "multiset_of (ah @ a # at) = multiset_of (ah @ at) + {#a#}" (is "_ = ?ma + _")
+  have as: "mset (ah @ a # at) = mset (ah @ at) + {#a#}" (is "_ = ?ma + _")
     by (simp add: algebra_simps)
-  have bs: "multiset_of (bh @ b # bt) = multiset_of (bh @ bt) + {#b#}" (is "_ = ?mb + _")
+  have bs: "mset (bh @ b # bt) = mset (bh @ bt) + {#b#}" (is "_ = ?mb + _")
     by (simp add: algebra_simps)
   from lprod_list have "(?ma, ?mb) \<in> mult R"
     by auto
@@ -86,9 +86,9 @@
   assumes wf_R: "wf R"
   shows "wf (lprod R)"
 proof -
-  have subset: "lprod (R^+) \<subseteq> inv_image (mult (R^+)) multiset_of"
+  have subset: "lprod (R^+) \<subseteq> inv_image (mult (R^+)) mset"
     by (auto simp add: lprod_implies_mult trans_trancl)
-  note lprodtrancl = wf_subset[OF wf_inv_image[where r="mult (R^+)" and f="multiset_of", 
+  note lprodtrancl = wf_subset[OF wf_inv_image[where r="mult (R^+)" and f="mset", 
     OF wf_mult[OF wf_trancl[OF wf_R]]], OF subset]
   note lprod = wf_subset[OF lprodtrancl, where p="lprod R", OF lprod_subset, simplified]
   show ?thesis by (auto intro: lprod)
diff -r 78a82c37b4b2 -r 484559628038 src/HOL/ex/Bubblesort.thy
--- a/src/HOL/ex/Bubblesort.thy	Thu Jun 18 16:17:51 2015 +0200
+++ b/src/HOL/ex/Bubblesort.thy	Fri Jun 19 15:55:22 2015 +0200
@@ -41,7 +41,7 @@
     by(auto simp: size_bubble_min dest!: bubble_minD_size split: list.splits if_splits)
 qed
 
-lemma mset_bubble_min: "multiset_of (bubble_min xs) = multiset_of xs"
+lemma mset_bubble_min: "mset (bubble_min xs) = mset xs"
 apply(induction xs rule: bubble_min.induct)
   apply simp
  apply simp
@@ -49,19 +49,19 @@
 done
 
 lemma bubble_minD_mset:
-  "bubble_min (xs) = ys \<Longrightarrow> multiset_of xs = multiset_of ys"
+  "bubble_min (xs) = ys \<Longrightarrow> mset xs = mset ys"
 by(auto simp: mset_bubble_min)
 
 lemma mset_bubblesort:
-  "multiset_of (bubblesort xs) = multiset_of xs"
+  "mset (bubblesort xs) = mset xs"
 apply(induction xs rule: bubblesort.induct)
   apply simp
  apply simp
 by(auto split: list.splits if_splits dest: bubble_minD_mset)
-  (metis add_eq_conv_ex mset_bubble_min multiset_of.simps(2))
+  (metis add_eq_conv_ex mset_bubble_min mset.simps(2))
 
 lemma set_bubblesort: "set (bubblesort xs) = set xs"
-by(rule mset_bubblesort[THEN multiset_of_eq_setD])
+by(rule mset_bubblesort[THEN mset_eq_setD])
 
 lemma bubble_min_min: "bubble_min xs = y#ys \<Longrightarrow> z \<in> set ys \<Longrightarrow> y \<le> z"
 apply(induction xs arbitrary: y ys z rule: bubble_min.induct)
diff -r 78a82c37b4b2 -r 484559628038 src/HOL/ex/MergeSort.thy
--- a/src/HOL/ex/MergeSort.thy	Thu Jun 18 16:17:51 2015 +0200
+++ b/src/HOL/ex/MergeSort.thy	Fri Jun 19 15:55:22 2015 +0200
@@ -19,8 +19,8 @@
 | "merge xs [] = xs"
 | "merge [] ys = ys"
 
-lemma multiset_of_merge [simp]:
-  "multiset_of (merge xs ys) = multiset_of xs + multiset_of ys"
+lemma mset_merge [simp]:
+  "mset (merge xs ys) = mset xs + mset ys"
   by (induct xs ys rule: merge.induct) (simp_all add: ac_simps)
 
 lemma set_merge [simp]:
@@ -42,14 +42,14 @@
   "sorted (msort xs)"
   by (induct xs rule: msort.induct) simp_all
 
-lemma multiset_of_msort:
-  "multiset_of (msort xs) = multiset_of xs"
+lemma mset_msort:
+  "mset (msort xs) = mset xs"
   by (induct xs rule: msort.induct)
-    (simp_all, metis append_take_drop_id drop_Suc_Cons multiset_of.simps(2) multiset_of_append take_Suc_Cons)
+    (simp_all, metis append_take_drop_id drop_Suc_Cons mset.simps(2) mset_append take_Suc_Cons)
 
 theorem msort_sort:
   "sort = msort"
-  by (rule ext, rule properties_for_sort) (fact multiset_of_msort sorted_msort)+
+  by (rule ext, rule properties_for_sort) (fact mset_msort sorted_msort)+
 
 end
 
diff -r 78a82c37b4b2 -r 484559628038 src/HOL/ex/Quicksort.thy
--- a/src/HOL/ex/Quicksort.thy	Thu Jun 18 16:17:51 2015 +0200
+++ b/src/HOL/ex/Quicksort.thy	Fri Jun 19 15:55:22 2015 +0200
@@ -21,7 +21,7 @@
   by (simp_all add: not_le)
 
 lemma quicksort_permutes [simp]:
-  "multiset_of (quicksort xs) = multiset_of xs"
+  "mset (quicksort xs) = mset xs"
   by (induct xs rule: quicksort.induct) (simp_all add: ac_simps)
 
 lemma set_quicksort [simp]: "set (quicksort xs) = set xs"