diff -r 860c65c7388a -r 17403c5a9eb1 doc-src/TutorialI/Overview/RECDEF.thy
--- a/doc-src/TutorialI/Overview/RECDEF.thy	Fri Mar 30 16:12:57 2001 +0200
+++ b/doc-src/TutorialI/Overview/RECDEF.thy	Fri Mar 30 18:12:26 2001 +0200
@@ -75,4 +75,11 @@
 apply(simp add:rev_map sym[OF map_compose] cong:map_cong)
 done
 
+text{*
+\begin{exercise}
+Define a function for merging two ordered lists (of natural numbers) and
+show that if the two input lists are ordered, so is the output.
+\end{exercise}
+*}
+
 end