# HG changeset patch
# User nipkow
# Date 1659438959 -7200
# Node ID a480964ea704891c5675d8789e0f91a6055c867b
# Parent  1635ee32e6d823d7cee176e5fc2e0d2d953b62d7
show sum_list defn

diff -r 1635ee32e6d8 -r a480964ea704 src/Doc/Prog_Prove/Types_and_funs.thy
--- a/src/Doc/Prog_Prove/Types_and_funs.thy	Fri Jul 29 08:45:51 2022 +0200
+++ b/src/Doc/Prog_Prove/Types_and_funs.thy	Tue Aug 02 13:15:59 2022 +0200
@@ -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>