--- a/src/HOL/Library/Permutation.thy Sat Dec 17 15:22:00 2016 +0100
+++ b/src/HOL/Library/Permutation.thy Sat Dec 17 15:22:13 2016 +0100
@@ -134,7 +134,7 @@
apply simp
done
-proposition mset_le_perm_append: "mset xs \<le># mset ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
+proposition mset_le_perm_append: "mset xs \<subseteq># mset ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
apply (auto simp: mset_eq_perm[THEN sym] mset_subset_eq_exists_conv)
apply (insert surj_mset)
apply (drule surjD)