src/ZF/Induct/Multiset.thy

--- a/src/ZF/Induct/Multiset.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Induct/Multiset.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -393,7 +393,7 @@
 done
 
 lemma msize_eq_succ_imp_elem: "\<lbrakk>msize(M)= $# succ(n); n \<in> nat\<rbrakk> \<Longrightarrow> \<exists>a. a \<in> mset_of(M)"
-apply (unfold msize_def)
+  unfolding msize_def
 apply (blast dest: setsum_succD)
 done
 
@@ -480,7 +480,7 @@
   (\<forall>a \<in> mset_of(M). setsum(\<lambda>z. $# mcount(M(a:=M`a #- 1), z), A) =
   (if a \<in> A then setsum(\<lambda>z. $# mcount(M, z), A) $- #1
            else setsum(\<lambda>z. $# mcount(M, z), A))))"
-apply (unfold multiset_def)
+  unfolding multiset_def
 apply (erule Finite_induct)
 apply (auto simp add: multiset_fun_iff)
 apply (unfold mset_of_def mcount_def)