# 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 \ '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 \ nat"} +Then define a function @{text "sum_tree ::"} @{typ "nat tree \ 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}