src/ZF/Induct/Multiset.thy
changeset 76217 8655344f1cf6
parent 76216 9fc34f76b4e8
child 80754 701912f5645a
--- a/src/ZF/Induct/Multiset.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Induct/Multiset.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -268,12 +268,12 @@
 by (auto intro!: lam_cong simp add: munion_def)
 
 lemma munion_assoc: "(M +# N) +# K = M +# (N +# K)"
-apply (unfold munion_def mset_of_def)
+  unfolding munion_def mset_of_def
 apply (rule lam_cong, auto)
 done
 
 lemma munion_lcommute: "M +# (N +# K) = N +# (M +# K)"
-apply (unfold munion_def mset_of_def)
+  unfolding munion_def mset_of_def
 apply (rule lam_cong, auto)
 done
 
@@ -291,7 +291,7 @@
 by (auto simp add: multiset_def mdiff_def normalize_def multiset_fun_iff mset_of_def funrestrict_def)
 
 lemma mdiff_union_inverse2 [simp]: "multiset(M) \<Longrightarrow> M +# {#a#} -# {#a#} = M"
-apply (unfold multiset_def munion_def mdiff_def msingle_def normalize_def mset_of_def)
+  unfolding multiset_def munion_def mdiff_def msingle_def normalize_def mset_of_def
 apply (auto cong add: if_cong simp add: ltD multiset_fun_iff funrestrict_def subset_Un_iff2 [THEN iffD1])
 prefer 2 apply (force intro!: lam_type)
 apply (subgoal_tac [2] "{x \<in> A \<union> {a} . x \<noteq> a \<and> x \<in> A} = A")
@@ -483,7 +483,7 @@
   unfolding multiset_def
 apply (erule Finite_induct)
 apply (auto simp add: multiset_fun_iff)
-apply (unfold mset_of_def mcount_def)
+  unfolding mset_of_def mcount_def
 apply (case_tac "x \<in> A", auto)
 apply (subgoal_tac "$# M ` x $+ #-1 = $# M ` x $- $# 1")
 apply (erule ssubst)