src/HOL/Library/Permutation.thy
changeset 64587 8355a6e2df79
parent 63649 e690d6f2185b
child 69597 ff784d5a5bfb
     1.1 --- a/src/HOL/Library/Permutation.thy	Sat Dec 17 15:22:00 2016 +0100
     1.2 +++ b/src/HOL/Library/Permutation.thy	Sat Dec 17 15:22:13 2016 +0100
     1.3 @@ -134,7 +134,7 @@
     1.4    apply simp
     1.5    done
     1.6  
     1.7 -proposition mset_le_perm_append: "mset xs \<le># mset ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
     1.8 +proposition mset_le_perm_append: "mset xs \<subseteq># mset ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
     1.9    apply (auto simp: mset_eq_perm[THEN sym] mset_subset_eq_exists_conv)
    1.10    apply (insert surj_mset)
    1.11    apply (drule surjD)