--- a/ProgTutorial/FirstSteps.thy	Tue Aug 18 01:05:56 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Wed Aug 19 00:49:40 2009 +0200
@@ -1167,6 +1167,31 @@
   in @{ML_file "HOL/Tools/hologic.ML"}.
   \end{readmore}
 
+  \begin{exercise}\label{ex:debruijn}
+  Implement the function,\footnote{Personal communication of
+  de Bruijn to Dyckhoff.} called deBruijn n, that constructs terms of the form:
+  
+  \begin{center}
+  \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
+  {\it rhs n} & $\dn$ & $\bigwedge${\it i=1\ldots n.  P\,i}\\
+  {\it lhs n} & $\dn$ & $\bigwedge${\it i=1\ldots n. P\,i = P (i + 1 mod n)}
+                        $\longrightarrow$ {\it rhs n}\\
+  {\it deBruijn n} & $\dn$ & {\it lhs n} $\longrightarrow$ {\it rhs n}\\
+  \end{tabular}
+  \end{center}
+
+  For n=3 this function returns the term
+
+  \begin{center}
+  \begin{tabular}{l}
+  (P 2 = P 3 $\longrightarrow$ P 3 $\wedge$ P 2 $\wedge$ P 1) $\wedge$\\
+  (P 1 = P 2 $\longrightarrow$ P 3 $\wedge$ P 2 $\wedge$ P 1) $\wedge$\\ 
+  (P 1 = P 3 $\longrightarrow$ P 3 $\wedge$ P 2 $\wedge$ P 1) $\longrightarrow$ P 3 $\wedge$ P 2 $\wedge$ P 1
+  \end{tabular}
+  \end{center}
+
+  \end{exercise}
+
   When constructing terms manually, there are a few subtle issues with
   constants. They usually crop up when pattern matching terms or types, or
   when constructing them. While it is perfectly ok to write the function