diff -r 6cb700c77786 -r dbac0ebb4a85 src/Doc/Prog_Prove/Logic.thy
--- 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}