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