# HG changeset patch
# User griff
# Date 1248170021 -7200
# Node ID 83abec9070725e4c5a4017f37abdc09b31b8fb36
# Parent  29787dcf7b2eedfae6bf2f6226429c6a19533e8c
if n would be 0, rev_sum would be missing an argument

diff -r 29787dcf7b2e -r 83abec907072 ProgTutorial/FirstSteps.thy
--- 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. 
diff -r 29787dcf7b2e -r 83abec907072 progtutorial.pdf
Binary file progtutorial.pdf has changed