diff -r 1c17e99f6f66 -r 9da9ba2b095b CookBook/Solutions.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Solutions.thy	Thu Oct 02 04:48:41 2008 -0400
@@ -0,0 +1,29 @@
+theory Solutions
+imports Main
+uses "antiquote_setup.ML"
+     "antiquote_setup_plus.ML"
+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
\ No newline at end of file