src/HOL/Library/Permutation.thy
changeset 60397 f8a513fedb31
parent 58881 b9556a055632
child 60495 d7ff0a1df90a
child 60500 903bb1495239
     1.1 --- a/src/HOL/Library/Permutation.thy	Mon Jun 08 22:04:19 2015 +0200
     1.2 +++ b/src/HOL/Library/Permutation.thy	Wed Jun 10 13:24:16 2015 +0200
     1.3 @@ -140,7 +140,7 @@
     1.4    apply simp
     1.5    done
     1.6  
     1.7 -lemma multiset_of_le_perm_append: "multiset_of xs \<le> multiset_of ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
     1.8 +lemma multiset_of_le_perm_append: "multiset_of xs \<le># multiset_of ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
     1.9    apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv)
    1.10    apply (insert surj_multiset_of)
    1.11    apply (drule surjD)