--- a/ProgTutorial/FirstSteps.thy Mon Apr 13 08:30:48 2009 +0000
+++ b/ProgTutorial/FirstSteps.thy Tue Jul 21 11:53:41 2009 +0200
@@ -795,7 +795,7 @@
\begin{exercise}\label{fun:revsum}
Write a function @{text "rev_sum : term -> term"} that takes a
- term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "n"} might be zero)
+ term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "n"} might be one)
and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume
the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"}
associates to the left. Try your function on some examples.