src/HOL/Library/Permutation.thy
changeset 35272 c283ae736bea
parent 33498 318acc1c9399
child 36903 489c1fbbb028
     1.1 --- a/src/HOL/Library/Permutation.thy	Mon Feb 22 09:15:10 2010 +0100
     1.2 +++ b/src/HOL/Library/Permutation.thy	Mon Feb 22 09:15:10 2010 +0100
     1.3 @@ -154,7 +154,7 @@
     1.4    done
     1.5  
     1.6  lemma multiset_of_le_perm_append:
     1.7 -    "(multiset_of xs \<le># multiset_of ys) = (\<exists>zs. xs @ zs <~~> ys)"
     1.8 +    "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, drule surjD)
    1.11    apply (blast intro: sym)+