--- a/ProgTutorial/Essential.thy Fri Aug 13 18:05:30 2010 +0800
+++ b/ProgTutorial/Essential.thy Fri Aug 13 18:42:58 2010 +0800
@@ -632,6 +632,14 @@
number representing their sum.
\end{exercise}
+ \begin{exercise}\label{fun:makelist}
+ Write a function that takes an integer @{text i} and
+ produces an Isabelle integer list from @{text 1} upto @{text i},
+ and then builds the reverse of this list using @{const rev}.
+ The relevant helper functions are @{ML upto},
+ @{ML HOLogic.mk_number} and @{ML HOLogic.mk_list}.
+ \end{exercise}
+
\begin{exercise}\label{ex:debruijn}
Implement the function, which we below name deBruijn, that depends on a natural
number n$>$0 and constructs terms of the form: