# HG changeset patch
# User nipkow
# Date 1484054980 -3600
# Node ID 2baa926a958d7952ca5a38cf6db30e390146a1f1
# Parent  9e8de30fd8598df673a0fdf6f399e67091fe8a2e
tuned

diff -r 9e8de30fd859 -r 2baa926a958d src/Doc/Prog_Prove/Types_and_funs.thy
--- 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}