# HG changeset patch
# User paulson
# Date 1659439166 -3600
# Node ID b93ed38cef8517027de0645aaabe9d094bf6b4eb
# Parent  a480964ea704891c5675d8789e0f91a6055c867b# Parent  f6695e7aff321c0c2b2bab47ca02b75288b5e381
merged

diff -r f6695e7aff32 -r b93ed38cef85 src/Doc/Prog_Prove/Types_and_funs.thy
--- a/src/Doc/Prog_Prove/Types_and_funs.thy	Tue Aug 02 12:19:05 2022 +0100
+++ b/src/Doc/Prog_Prove/Types_and_funs.thy	Tue Aug 02 12:19:26 2022 +0100
@@ -220,7 +220,9 @@
 Then define a function \<open>sum_tree ::\<close> \<^typ>\<open>nat tree \<Rightarrow> nat\<close>
 that sums up all values in a tree of natural numbers
 and prove \<^prop>\<open>sum_tree t = sum_list(contents t)\<close>
-(where \<^const>\<open>sum_list\<close> is predefined).
+where \<^const>\<open>sum_list\<close> is predefined by the equations
+@{thm sum_list.Nil[where 'a=nat]} and
+@{thm sum_list.Cons}.
 \end{exercise}
 
 \begin{exercise}
@@ -272,8 +274,7 @@
 empty. Note that \<^const>\<open>itrev\<close> is tail-recursive: it can be
 compiled into a loop; no stack is necessary for executing it.
 
-Naturally, we would like to show that \<^const>\<open>itrev\<close> does indeed reverse
-its first argument provided the second one is empty:
+Naturally, we would like to show that \<^const>\<open>itrev\<close> reverses its first argument:
 \<close>
 
 lemma "itrev xs [] = rev xs"
@@ -323,7 +324,7 @@
 (*>*)
 apply(induction xs arbitrary: ys)
 
-txt\<open>The induction hypothesis in the induction step is now universally quantified over \<open>ys\<close>:
+txt\<open>The induction hypothesis is now universally quantified over \<open>ys\<close>:
 @{subgoals[display,margin=65]}
 Thus the proof succeeds:
 \<close>