tuned
authornipkow
Tue Jan 10 14:29:40 2017 +0100 (2017-01-10)
changeset 648622baa926a958d
parent 64861 9e8de30fd859
child 64869 a73ac9558220
tuned
src/Doc/Prog_Prove/Types_and_funs.thy
     1.1 --- a/src/Doc/Prog_Prove/Types_and_funs.thy	Tue Jan 10 11:37:18 2017 +0100
     1.2 +++ b/src/Doc/Prog_Prove/Types_and_funs.thy	Tue Jan 10 14:29:40 2017 +0100
     1.3 @@ -218,9 +218,10 @@
     1.4  a function @{text "contents ::"} @{typ "'a tree \<Rightarrow> 'a list"}
     1.5  that collects all values in a tree in a list, in any order,
     1.6  without removing duplicates.
     1.7 -Then define a function @{text "treesum ::"} @{typ "nat tree \<Rightarrow> nat"}
     1.8 +Then define a function @{text "sum_tree ::"} @{typ "nat tree \<Rightarrow> nat"}
     1.9  that sums up all values in a tree of natural numbers
    1.10 -and prove @{prop "treesum t = listsum(contents t)"}.
    1.11 +and prove @{prop "sum_tree t = sum_list(contents t)"}
    1.12 +(where @{const sum_list} is predefined).
    1.13  \end{exercise}
    1.14  
    1.15  \begin{exercise}