
diff -r 2f39df9ceb63 -r 4c32349b9875 ProgTutorial/Essential.thy
--- 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:




