--- a/ProgTutorial/Solutions.thy Fri Aug 13 18:05:30 2010 +0800
+++ b/ProgTutorial/Solutions.thy Fri Aug 13 18:42:58 2010 +0800
@@ -35,6 +35,15 @@
ML{*fun make_sum t1 t2 =
HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *}
+
+text {* \solution{fun:makelist} *}
+
+ML{*fun mk_rev_upto i =
+ 1 upto i
+ |> map (HOLogic.mk_number @{typ int})
+ |> HOLogic.mk_list @{typ int}
+ |> curry (op $) @{term "rev :: int list \<Rightarrow> int list"}*}
+
text {* \solution{ex:debruijn} *}
ML{*fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n)