theory Solutions
imports Base
begin

chapter {* Solutions to Most Exercises *}

text {* \solution{fun:revsum} *}

ML {* 
fun rev_sum t =
let
 fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u
   | dest_sum u = [u]
 in
   foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t)
 end;
*}

text {* \solution{fun:makesum} *}

ML {*
fun make_sum t1 t2 =
    HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2)
*}

end