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: