author nipkow Fri, 12 Nov 2021 16:09:35 +0100 changeset 74764 adb10e840b71 parent 74762 8362a5b2c2dd (current diff) parent 74763 dbac0ebb4a85 (diff) child 74772 2b212c8138a5
merged
--- 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}
--- 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>