--- a/ProgTutorial/Base.thy	Thu Nov 19 17:48:44 2009 +0100
+++ b/ProgTutorial/Base.thy	Thu Nov 19 20:00:10 2009 +0100
@@ -8,7 +8,6 @@
 notation (latex output)
   Cons ("_ # _" [66,65] 65)
 
-
 (* rebinding of writeln and tracing so that it can *)
 (* be compared in intiquotations                   *)
 ML {* 
@@ -141,6 +140,19 @@
          IsarCmd.local_setup (txt, pos) #> write_file_lsetup_blk txt));
 *}
 
+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))
+*}
 
 use "output_tutorial.ML"
 use "antiquote_setup.ML"