# HG changeset patch
# User nipkow
# Date 1711638868 -3600
# Node ID f8d7df38d7c668946e1e12984f0948f5501f2b39
# Parent  44d8fb3da9d5e675ffdc4a90fa7f8b0e1833efee
tuned

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