--- a/src/HOL/Library/Permutation.thy Mon Jun 08 22:04:19 2015 +0200
+++ b/src/HOL/Library/Permutation.thy Wed Jun 10 13:24:16 2015 +0200
@@ -140,7 +140,7 @@
apply simp
done
-lemma multiset_of_le_perm_append: "multiset_of xs \<le> multiset_of ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
+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)
apply (drule surjD)