author nipkow Fri, 12 Nov 2021 16:09:19 +0100 changeset 74763 dbac0ebb4a85 parent 74761 6cb700c77786 child 74764 adb10e840b71
 src/Doc/Prog_Prove/Logic.thy file | annotate | diff | comparison | revisions src/Doc/Prog_Prove/Types_and_funs.thy file | annotate | diff | comparison | revisions
--- 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}
--- 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>