diff -r 44d8fb3da9d5 -r f8d7df38d7c6 src/Doc/Prog_Prove/Isar.thy
--- a/src/Doc/Prog_Prove/Isar.thy	Thu Mar 28 13:33:10 2024 +0000
+++ b/src/Doc/Prog_Prove/Isar.thy	Thu Mar 28 16:14:28 2024 +0100
@@ -115,7 +115,7 @@
 If you wonder why \<open>2\<close> directly implies \<open>False\<close>: from \<open>2\<close>
 it follows that \<^prop>\<open>a \<notin> f a \<longleftrightarrow> a \<in> f a\<close>.
 
-\subsection{\indexed{\<open>this\<close>}{this}, \indexed{\isacom{then}}{then}, \indexed{\isacom{hence}}{hence} and \indexed{\isacom{thus}}{thus}}
+\subsection{\indexed{\<open>this\<close>}{this}, \indexed{\isacom{then}}{then}, \indexed{\isacom{with}}{with}, \indexed{\isacom{hence}}{hence}, \indexed{\isacom{thus}}{thus}, \indexed{\isacom{using}}{using}}
 
 Labels should be avoided. They interrupt the flow of the reader who has to
 scan the context for the point where the label was introduced. Ideally, the
@@ -197,8 +197,7 @@
 \<close>
 
 proof -
-  have "\<exists> a. {x. x \<notin> f x} = f a" using s
-    by(auto simp: surj_def)
+  have "\<exists> a. {x. x \<notin> f x} = f a" using s by(auto simp: surj_def)
   thus "False" by blast
 qed