--- 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