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/Combinatorics/Multiset_Permutations.thy
changeset 74362 0135a0c77b64
parent 73477 1d8a79aa2a99 
--- a/src/HOL/Combinatorics/Multiset_Permutations.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Combinatorics/Multiset_Permutations.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -131,7 +131,7 @@
 
 lemma permutations_of_multiset_not_empty [simp]: "permutations_of_multiset A \<noteq> {}"
 proof -
-  from ex_mset[of A] guess xs ..
+  from ex_mset[of A] obtain xs where "mset xs = A" ..
   thus ?thesis by (auto simp: permutations_of_multiset_def)
 qed
 
@@ -142,7 +142,8 @@
   from ex_mset[of A] obtain ys where ys: "mset ys = A" ..
   with A have "mset xs = mset (map f ys)" 
     by (simp add: permutations_of_multiset_def)
-  from mset_eq_permutation[OF this] guess \<sigma> . note \<sigma> = this
+  then obtain \<sigma> where \<sigma>: "\<sigma> permutes {..<length (map f ys)}" "permute_list \<sigma> (map f ys) = xs"
+    by (rule mset_eq_permutation)
   with ys have "xs = map f (permute_list \<sigma> ys)"
     by (simp add: permute_list_map)
   moreover from \<sigma> ys have "permute_list \<sigma> ys \<in> permutations_of_multiset A"
isabelle