
diff -r 2f39df9ceb63 -r 4c32349b9875 ProgTutorial/Solutions.thy
--- 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) 




