--- a/CookBook/FirstSteps.thy	Wed Oct 01 20:42:55 2008 -0400
+++ b/CookBook/FirstSteps.thy	Thu Oct 02 04:48:41 2008 -0400
@@ -1,27 +1,10 @@
 theory FirstSteps
 imports Main
 uses "antiquote_setup.ML"
+     "antiquote_setup_plus.ML"
 begin
 
 
-(*<*)
-
-
-ML {*
-local structure O = ThyOutput
-in
-  fun check_exists f = 
-    if File.exists (Path.explode ("~~/src/" ^ f)) then ()
-    else error ("Source file " ^ quote f ^ " does not exist.")
-  
-  val _ = O.add_commands
-   [("ML_file", O.args (Scan.lift Args.name) (O.output (fn _ => fn name =>
-         (check_exists name; Pretty.str name))))];
-
-end
-*}
-(*>*)
-
 chapter {* First Steps *}
 
 
@@ -56,8 +39,9 @@
   The expression inside \isacommand{ML} commands is immediately evaluated,
   like ``normal'' Isabelle proof scripts, by using the advance and undo buttons of 
   your Isabelle environment. The code inside the \isacommand{ML} command 
-  can also contain value- and function bindings. However on such ML-commands the 
-  undo operation behaves slightly counter-intuitive, because if you define
+  can also contain value and function bindings. However on such \isacommand{ML}
+  commands the undo operation behaves slightly counter-intuitive, because 
+  if you define
 *}
 
 ML {*
@@ -69,14 +53,14 @@
   @{ML "foo"}. 
 
   Once a portion of code is relatively stable, one usually wants to 
-  export it to a separate ML-file. Such files can be included in a 
-  theory using @{ML_text "uses"} in the header of the theory.
+  export it to a separate ML-file. Such files can then be included in a 
+  theory by using \isacommand{uses} in the header of the theory, like
 
   \begin{center}
   \begin{tabular}{@ {}l}
   \isacommand{theory} CookBook\\
   \isacommand{imports} Main\\
-  \isacommand{uses} @{text "\"file_to_be_included.ML\""}\\
+  \isacommand{uses} @{ML_text "\"file_to_be_included.ML\""} @{text "\<dots>"}\\
   \isacommand{begin}\\
   \ldots
   \end{tabular}
@@ -109,20 +93,18 @@
 
 text {* 
   The funtion warning should only be used for testing purposes, because
-  the problem with this function is that any output will be
-  overwritten if an error is raised. For anything more serious 
-  the function @{ML tracing}, which writes all output in a separate
-  buffer, should be used.
-
+  any output this funtion generated will be overwritten, if an error is raised. 
+  For printing anything more serious and elaborate, the function @{ML tracing}
+  should be used. This function writes all output in a separate buffer.
 *}
 
 ML {* tracing "foo" *}
 
-text {* (FIXME: complete the comment about redirecting the trace information) 
+text {* 
 
-  In Isabelle it is possible to redirect the message channels to a 
-  separate file, e.g. to prevent Proof General from choking on massive 
-  amounts of trace output.
+  It is also possible to redirect the channel where the @{ML_text "foo"} is 
+  printed to a separate file, e.g. to prevent Proof General from choking on massive 
+  amounts of trace output. This rediretion can be achieved using the code
 
 *}
 
@@ -141,6 +123,12 @@
      TextIO.flushOut stream));
 *}
 
+text {* 
+  Calling the @{ML_text "redirect_tracing"} function with @{ML_text "(TextIO.openOut \"foo.bar\")"} 
+  will cause that all tracing information is printed into the file @{ML_text "foo.bar"}.
+
+*}
+
 
 section {* Antiquotations *}
 
@@ -191,7 +179,7 @@
 
 *}
 
-section {* Terms *}
+section {* Terms and Types *}
 
 text {*
   One way to construct terms of Isabelle on the ML-level is by using the antiquotation 
@@ -238,7 +226,7 @@
   enough:
   \end{exercise}
 *}
-ML {* print_depth 50 *} 
+ML {* print_depth 50 *}
 
 text {*
   
@@ -250,21 +238,23 @@
 
 ML {* @{term "P x"} ; @{prop "P x"} *}
 
-text {* which needs the coercion and *}
+text {* which inserts the coercion in the latter ase and *}
 
 
 ML {* @{term "P x \<Longrightarrow> Q x"} ; @{prop "P x \<Longrightarrow> Q x"} *}
 
 text {* which does not. *}
 
-section {* Constructing Terms Manually *} 
+text {* (FIXME: add something about @{text "@{typ \<dots>}"}) *}
+
+section {* Constructing Terms and Types Manually *} 
 
 text {*
 
-  While antiquotations are very convenient for constructing terms, they can
-  only construct fixed terms. Unfortunately, one often needs to construct terms 
+  While antiquotations are very convenient for constructing terms (similarly types), 
+  they can only construct fixed terms. Unfortunately, one often needs to construct them 
   dynamically. For example, a function that returns the implication 
-  @{text "\<And>(x::nat). P x \<Longrightarrow> Q x"} taking @{term P} and @{term Q} as input terms 
+  @{text "\<And>(x::nat). P x \<Longrightarrow> Q x"} taking @{term P} and @{term Q} as arguments
   can only be written as
 *}
 
@@ -281,7 +271,7 @@
 text {*
 
   The reason is that one cannot pass the arguments @{term P} and @{term Q} into 
-  an antiquotation, like   
+  an antiquotation. For example this following does not work.
 *}
 
 ML {*
@@ -290,19 +280,21 @@
 
 text {*
 
-  To see the difference apply @{text "@{term S}"} and 
-  @{text "@{term T}"} to the functions.
+  To see this apply @{text "@{term S}"} and @{text "@{term T}"} to boths functions.
   
-
   One tricky point in constructing terms by hand is to obtain the fully qualified 
-  names for constants. For example the names for @{text "zero"} or @{text "+"} are
-  more complex than one first expects, namely @{ML_text "HOL.zero_class.zero"} 
-  and @{ML_text "HOL.plus_class.plus"}. The extra prefixes @{ML_text zero_class} 
-  and @{ML_text plus_class} are present because these constants are defined 
-  within type classes; the prefix @{text "HOL"} indicates in which theory they are 
-  defined. Guessing such internal names can sometimes be quite hard. Therefore 
-  Isabellle provides the antiquotation @{text "@{const_name \<dots>}"} does the expansion 
-  automatically, for example:
+  name for constants. For example the names for @{text "zero"} or @{text "+"} are
+  more complex than one first expects, namely 
+
+  \begin{center}
+  @{ML_text "HOL.zero_class.zero"} and @{ML_text "HOL.plus_class.plus"}. 
+  \end{center}
+  
+  The extra prefixes @{ML_text zero_class} and @{ML_text plus_class} are present because 
+  these constants are defined within type classes; the prefix @{text "HOL"} indicates in 
+  which theory they are defined. Guessing such internal names can sometimes be quite hard. 
+  Therefore Isabellle provides the antiquotation @{text "@{const_name \<dots>}"} which does the 
+  expansion automatically, for example:
 
 *}
 
@@ -328,21 +320,8 @@
   the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} 
   associates to the left. Try your function on some examples. 
   \end{exercise}
-*}
 
-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 {*
-  \begin{exercise}
+  \begin{exercise}\label{fun:makesum}
   Write a function which takes two terms representing natural numbers
   in unary (like @{term "Suc (Suc (Suc 0))"}), and produce the unary
   number representing their sum.
@@ -350,19 +329,11 @@
 
 *}
 
-ML {*
-  fun make_sum t1 t2 =
-      HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2)
-*}
-
-
 
 section {* Type Checking *}
 
 text {* 
   
-  (FIXME: Should we say something about types?)
-
   We can freely construct and manipulate terms, since they are just
   arbitrary unchecked trees. However, we eventually want to see if a
   term is well-formed, or type checks, relative to a theory.

--- a/CookBook/ROOT.ML	Wed Oct 01 20:42:55 2008 -0400
+++ b/CookBook/ROOT.ML	Thu Oct 02 04:48:41 2008 -0400
@@ -6,4 +6,6 @@
 
 use_thy "Appendix";
 use_thy "Recipes/NamedThms";
-use_thy "Recipes/Transformation";
\ No newline at end of file
+use_thy "Recipes/Transformation";
+
+use_thy "Solutions";
\ No newline at end of file

--- a/CookBook/Recipes/NamedThms.thy	Wed Oct 01 20:42:55 2008 -0400
+++ b/CookBook/Recipes/NamedThms.thy	Thu Oct 02 04:48:41 2008 -0400
@@ -1,9 +1,10 @@
 
 theory NamedThms
 imports Main
+uses "antiquote_setup.ML"
+     "antiquote_setup_plus.ML"
 begin
 
-
 section {* Accumulate a List of Theorems under a Name *} 
 
 
@@ -53,6 +54,12 @@
   \end{readmore}
  *}
 
+text {*
+  (FIXME: maybe add a comment about the case when the theorems 
+  to be added need to satisfy certain properties)
+
+*}
+
 
 end
   

--- /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

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/antiquote_setup_plus.ML	Thu Oct 02 04:48:41 2008 -0400
@@ -0,0 +1,16 @@
+(*
+Auxiliary antiquotations for the Cookbook.
+
+*)
+
+local structure O = ThyOutput
+in
+  fun check_exists f = 
+    if File.exists (Path.explode ("~~/src/" ^ f)) then ()
+    else error ("Source file " ^ quote f ^ " does not exist.")
+  
+  val _ = O.add_commands
+   [("ML_file", O.args (Scan.lift Args.name) (O.output (fn _ => fn name =>
+         (check_exists name; Pretty.str name))))];
+
+end
\ No newline at end of file

--- a/CookBook/document/root.tex	Wed Oct 01 20:42:55 2008 -0400
+++ b/CookBook/document/root.tex	Thu Oct 02 04:48:41 2008 -0400
@@ -22,7 +22,6 @@
 % sane default for proof documents
 \parindent 0pt\parskip 0.6ex
 
-
 % for comments on the margin
 \newcommand{\readmoremarginpar}[1]%
 {\marginpar[\raggedleft\small{#1}]{\raggedright\small{#1}}}
@@ -30,8 +29,9 @@
 \newenvironment{readmore}%
 {\hspace{-3pt}\readmoremarginpar{\fbox{\textbf{Read More}}}\it}{}
 
+% for exercises and comments
 \newtheorem{exercise}{Exercise}[section]
-
+\newcommand{\solution}[1]{{\bf Solution for Exercise~\ref{#1}.}}
 
 \begin{document}
 

Binary file cookbook.pdf has changed