# HG changeset patch
# User wenzelm
# Date 1666462536 -7200
# Node ID 2c0f252fb11cc009e5e582241efe492e8f30aaf1
# Parent  2b204e11141c2dfa27cba434a30a78ab254adc5b# Parent  f7174238b5e3cf015c252fd4f200711ed672bfc9
merged

diff -r f7174238b5e3 -r 2c0f252fb11c src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat Oct 22 20:06:55 2022 +0200
+++ b/src/HOL/Library/Multiset.thy	Sat Oct 22 20:15:36 2022 +0200
@@ -2002,13 +2002,12 @@
   by (induct xs) simp_all
 
 lemma surj_mset: "surj mset"
-apply (unfold surj_def)
-apply (rule allI)
-apply (rule_tac M = y in multiset_induct)
- apply auto
-apply (rule_tac x = "x # xa" in exI)
-apply auto
-done
+  unfolding surj_def
+proof (rule allI)
+  fix M
+  show "\<exists>xs. M = mset xs"
+    by (induction M) (auto intro: exI[of _ "_ # _"])
+qed
 
 lemma distinct_count_atmost_1:
   "distinct x = (\<forall>a. count (mset x) a = (if a \<in> set x then 1 else 0))"