--- a/ProgTutorial/Solutions.thy	Tue Aug 18 01:05:56 2009 +0200
+++ b/ProgTutorial/Solutions.thy	Wed Aug 19 00:49:40 2009 +0200
@@ -4,6 +4,20 @@
 
 chapter {* Solutions to Most Exercises\label{ch:solutions} *}
 
+text {* \solution{ex:debruijn} *}
+
+ML{*fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) 
+
+fun rhs 1 = P 1
+  | rhs n = HOLogic.mk_conj (P n, rhs (n - 1))
+
+fun lhs 1 n = HOLogic.mk_imp (HOLogic.mk_eq (P 1, P n), rhs n)
+  | lhs m n = HOLogic.mk_conj (HOLogic.mk_imp 
+                 (HOLogic.mk_eq (P (m - 1), P m), rhs n), lhs (m - 1) n)
+
+fun de_bruijn n =
+  HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))*}
+
 text {* \solution{fun:revsum} *}
 
 ML{*fun rev_sum ((p as Const (@{const_name plus}, _)) $ t $ u) =