# HG changeset patch
# User nipkow
# Date 1636729775 -3600
# Node ID adb10e840b712031d08ed4472315c33b0b4973b5
# Parent  8362a5b2c2dda1a04544e0a7210a514f63571b83# Parent  dbac0ebb4a8518537a8e3792a7630f948e437dfd
merged

diff -r 8362a5b2c2dd -r adb10e840b71 src/Doc/Prog_Prove/Logic.thy
--- a/src/Doc/Prog_Prove/Logic.thy	Fri Nov 12 08:51:45 2021 +0100
+++ b/src/Doc/Prog_Prove/Logic.thy	Fri Nov 12 16:09:35 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}
diff -r 8362a5b2c2dd -r adb10e840b71 src/Doc/Prog_Prove/Types_and_funs.thy
--- a/src/Doc/Prog_Prove/Types_and_funs.thy	Fri Nov 12 08:51:45 2021 +0100
+++ b/src/Doc/Prog_Prove/Types_and_funs.thy	Fri Nov 12 16:09:35 2021 +0100
@@ -171,7 +171,7 @@
 This customized induction rule can simplify inductive proofs. For example,
 \<close>
 
-lemma "div2(n) = n div 2"
+lemma "div2 n = n div 2"
 apply(induction n rule: div2.induct)
 
 txt\<open>(where the infix \<open>div\<close> is the predefined division operation)
@@ -328,7 +328,7 @@
 Thus the proof succeeds:
 \<close>
 
-apply auto
+apply(auto)
 done
 
 text\<open>