added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
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