# HG changeset patch
# User wenzelm
# Date 1536344062 -7200
# Node ID e609c3dec6f828c0bc7dc5ffb74564bd23c62139
# Parent  35ea237696cf6337d8ea4802d360ba5d305b5a3f# Parent  fc5763d000e817a9813f1161bc97d6d941456241
merged

diff -r fc5763d000e8 -r e609c3dec6f8 src/Doc/Prog_Prove/Types_and_funs.thy
--- a/src/Doc/Prog_Prove/Types_and_funs.thy	Fri Sep 07 19:49:26 2018 +0200
+++ b/src/Doc/Prog_Prove/Types_and_funs.thy	Fri Sep 07 20:14:22 2018 +0200
@@ -539,12 +539,16 @@
 @{text "split: if_splits"} or @{text "split: t.splits"}.
 
 \ifsem\else
-\subsection{Converting Numerals to @{const Suc} Terms}
+\subsection{Rewriting \<open>let\<close> and Numerals}
+
+Let-expressions (@{term "let x = s in t"}) can be expanded explicitly with the simplification rule
+@{thm[source] Let_def}. The simplifier will not expand \<open>let\<close>s automatically in many cases.
 
-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.
+Numerals of type @{typ nat} can be converted to @{const Suc} terms with the simplification rule
+@{thm[source] numeral_eq_Suc}. This is required, for example, when a function that is defined
+by pattern matching with @{const Suc} is applied to a numeral: if \<open>f\<close> is defined by
+@{text "f 0 = ..."} and  @{text "f (Suc n) = ..."}, the simplifier cannot simplify \<open>f 2\<close> unless
+\<open>2\<close> is converted to @{term "Suc(Suc 0)"} (via @{thm[source] numeral_eq_Suc}).
 \fi
 
 \subsection*{Exercises}