diff -r 05cbe2430b76 -r 1ca2f41770cc ProgTutorial/Solutions.thy
--- a/ProgTutorial/Solutions.thy	Wed Aug 19 00:49:40 2009 +0200
+++ b/ProgTutorial/Solutions.thy	Wed Aug 19 09:25:49 2009 +0200
@@ -4,20 +4,6 @@
 
 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) = 
@@ -41,6 +27,20 @@
 ML{*fun make_sum t1 t2 =
       HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *}
 
+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{ex:scancmts} *}
 
 ML{*val any = Scan.one (Symbol.not_eof)