diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Induct/PropLog.thy
--- a/src/ZF/Induct/PropLog.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Induct/PropLog.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -180,7 +180,7 @@
 subsubsection \<open>Soundness of the rules wrt truth-table semantics\<close>
 
 theorem soundness: "H |- p \<Longrightarrow> H |= p"
-  apply (unfold logcon_def)
+    unfolding logcon_def
   apply (induct set: thms)
       apply auto
   done