# HG changeset patch
# User nipkow
# Date 1476703238 -7200
# Node ID 3faa948dc861bf07d8942f3d5b3ae544fb5c067a
# Parent  b9a1486e79be0124d540d4858e0a7a89137d2bfd
updated to setsum -> sum

diff -r b9a1486e79be -r 3faa948dc861 src/Doc/Prog_Prove/Bool_nat_list.thy
--- a/src/Doc/Prog_Prove/Bool_nat_list.thy	Mon Oct 17 11:46:22 2016 +0200
+++ b/src/Doc/Prog_Prove/Bool_nat_list.thy	Mon Oct 17 13:20:38 2016 +0200
@@ -453,9 +453,9 @@
 \end{exercise}
 
 \begin{exercise}
-Define a recursive function @{text "sum ::"} @{typ"nat \<Rightarrow> nat"} such that
-\mbox{@{text"sum n"}} @{text"="} @{text"0 + ... + n"} and prove
-@{prop" sum(n::nat) = n * (n+1) div 2"}.
+Define a recursive function @{text "sum_upto ::"} @{typ"nat \<Rightarrow> nat"} such that
+\mbox{@{text"sum_upto n"}} @{text"="} @{text"0 + ... + n"} and prove
+@{prop" sum_upto (n::nat) = n * (n+1) div 2"}.
 \end{exercise}
 *}
 (*<*)