--- a/src/Doc/Prog_Prove/Types_and_funs.thy Wed Sep 05 21:56:44 2018 +0200
+++ b/src/Doc/Prog_Prove/Types_and_funs.thy Thu Sep 06 16:50:00 2018 +0200
@@ -538,6 +538,14 @@
Splitting if or case-expressions in the assumptions requires
@{text "split: if_splits"} or @{text "split: t.splits"}.
+\ifsem\else
+\subsection{Converting Numerals to @{const Suc} Terms}
+
+Recursive functions on type @{typ nat} are often defined by pattern matching over @{text 0} and @{const Suc},
+e.g. @{text "f 0 = ..."} and @{text "f (Suc n) = ..."}. In order to simplify \<open>f 2\<close>, the \<open>2\<close>
+needs to be converted to @{term "Suc(Suc 0)"} first. The simplification rule @{thm[source] numeral_eq_Suc}
+converts all numerals to @{const Suc} terms.
+\fi
\subsection*{Exercises}