--- 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}
*}
(*<*)