src/HOL/Library/Permutation.thy
changeset 63310 caaacf37943f
parent 61699 a81dc5c4d6a9
child 63649 e690d6f2185b
     1.1 --- a/src/HOL/Library/Permutation.thy	Thu Jun 16 17:11:00 2016 +0200
     1.2 +++ b/src/HOL/Library/Permutation.thy	Fri Jun 17 12:37:43 2016 +0200
     1.3 @@ -135,7 +135,7 @@
     1.4    done
     1.5  
     1.6  proposition mset_le_perm_append: "mset xs \<le># mset ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
     1.7 -  apply (auto simp: mset_eq_perm[THEN sym] mset_le_exists_conv)
     1.8 +  apply (auto simp: mset_eq_perm[THEN sym] mset_subset_eq_exists_conv)
     1.9    apply (insert surj_mset)
    1.10    apply (drule surjD)
    1.11    apply (blast intro: sym)+