--- a/src/Doc/Prog_Prove/Types_and_funs.thy Tue Jan 10 11:37:18 2017 +0100
+++ b/src/Doc/Prog_Prove/Types_and_funs.thy Tue Jan 10 14:29:40 2017 +0100
@@ -218,9 +218,10 @@
a function @{text "contents ::"} @{typ "'a tree \<Rightarrow> 'a list"}
that collects all values in a tree in a list, in any order,
without removing duplicates.
-Then define a function @{text "treesum ::"} @{typ "nat tree \<Rightarrow> nat"}
+Then define a function @{text "sum_tree ::"} @{typ "nat tree \<Rightarrow> nat"}
that sums up all values in a tree of natural numbers
-and prove @{prop "treesum t = listsum(contents t)"}.
+and prove @{prop "sum_tree t = sum_list(contents t)"}
+(where @{const sum_list} is predefined).
\end{exercise}
\begin{exercise}