# HG changeset patch
# User nipkow
# Date 1636729759 -3600
# Node ID dbac0ebb4a8518537a8e3792a7630f948e437dfd
# Parent  6cb700c7778604ad4f47affeb34c76ad2e66a747
tuned (thanks to J. Villadsen)

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}
diff -r 6cb700c77786 -r dbac0ebb4a85 src/Doc/Prog_Prove/Types_and_funs.thy
--- a/src/Doc/Prog_Prove/Types_and_funs.thy	Fri Nov 12 00:28:00 2021 +0100
+++ b/src/Doc/Prog_Prove/Types_and_funs.thy	Fri Nov 12 16:09:19 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>