src/ZF/UNITY/Merge.thy
changeset 76216 9fc34f76b4e8
parent 76215 a642599ffdea
--- a/src/ZF/UNITY/Merge.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/Merge.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -85,18 +85,18 @@
 
 
 lemma (in merge) In_value_type [TC,simp]: "s \<in> state \<Longrightarrow> s`In(n) \<in> list(A)"
-apply (unfold state_def)
+  unfolding state_def
 apply (drule_tac a = "In (n)" in apply_type)
 apply auto
 done
 
 lemma (in merge) Out_value_type [TC,simp]: "s \<in> state \<Longrightarrow> s`Out \<in> list(A)"
-apply (unfold state_def)
+  unfolding state_def
 apply (drule_tac a = Out in apply_type, auto)
 done
 
 lemma (in merge) iOut_value_type [TC,simp]: "s \<in> state \<Longrightarrow> s`iOut \<in> list(nat)"
-apply (unfold state_def)
+  unfolding state_def
 apply (drule_tac a = iOut in apply_type, auto)
 done