--- a/src/Doc/Prog_Prove/Logic.thy Fri Nov 12 00:28:00 2021 +0100
+++ b/src/Doc/Prog_Prove/Logic.thy Fri Nov 12 16:09:19 2021 +0100
@@ -75,6 +75,8 @@
Theorems should be of the form \<open>\<lbrakk> A\<^sub>1; \<dots>; A\<^sub>n \<rbrakk> \<Longrightarrow> A\<close>,
not \<open>A\<^sub>1 \<and> \<dots> \<and> A\<^sub>n \<longrightarrow> A\<close>. Both are logically equivalent
but the first one works better when using the theorem in further proofs.
+
+The ASCII representation of \<open>\<lbrakk>\<close> and \<open>\<rbrakk>\<close> is \texttt{[|} and \texttt{|]}.
\end{warn}
\section{Sets}