src/ZF/ex/Limit.thy

--- a/src/ZF/ex/Limit.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/ex/Limit.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -470,7 +470,7 @@
 
 lemma matrix_chain_left:
     "\<lbrakk>matrix(D,M); n \<in> nat\<rbrakk> \<Longrightarrow> chain(D,M`n)"
-apply (unfold chain_def)
+  unfolding chain_def
 apply (auto intro: matrix_fun [THEN apply_type] matrix_in matrix_rel_0_1)
 done