Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Permutation.thy
changeset 35272 c283ae736bea
parent 33498 318acc1c9399
child 36903 489c1fbbb028 
--- a/src/HOL/Library/Permutation.thy	Mon Feb 22 09:15:10 2010 +0100
+++ b/src/HOL/Library/Permutation.thy	Mon Feb 22 09:15:10 2010 +0100
@@ -154,7 +154,7 @@
   done
 
 lemma multiset_of_le_perm_append:
-    "(multiset_of xs \<le># multiset_of ys) = (\<exists>zs. xs @ zs <~~> ys)"
+    "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, drule surjD)
   apply (blast intro: sym)+
isabelle