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 \ int list"}*} + text {* \solution{ex:debruijn} *} ML{*fun P n = @{term "P::nat \ bool"} $ (HOLogic.mk_number @{typ "nat"} n)