--- a/CookBook/FirstSteps.thy	Sat Nov 29 21:20:18 2008 +0000
+++ b/CookBook/FirstSteps.thy	Sat Dec 13 01:33:22 2008 +0000
@@ -7,9 +7,9 @@
 
 text {*
 
-  Isabelle programming is done in SML.  Just like lemmas and proofs, SML-code
+  Isabelle programming is done in ML.  Just like lemmas and proofs, ML-code
   in Isabelle is part of a theory. If you want to follow the code written in
-  this chapter, we assume you are working inside the theory defined by
+  this chapter, we assume you are working inside the theory starting with
 
   \begin{center}
   \begin{tabular}{@ {}l}
@@ -49,7 +49,7 @@
 
   \begin{center}
   \begin{tabular}{@ {}l}
-  \isacommand{theory} CookBook\\
+  \isacommand{theory} FirstSteps\\
   \isacommand{imports} Main\\
   \isacommand{uses} @{ML_text "\"file_to_be_included.ML\""} @{text "\<dots>"}\\
   \isacommand{begin}\\
@@ -82,12 +82,12 @@
   The function @{ML "warning"} should only be used for testing purposes, because any
   output this function generates will be overwritten as soon as an error is
   raised. For printing anything more serious and elaborate, the
-  function @{ML tracing} should be used. This function writes all output into
+  function @{ML tracing} is more appropriate. This function writes all output into
   a separate tracing buffer. For example
 
   @{ML [display] "tracing \"foo\""}
 
-  It is also possible to redirect the ``channel'' where the @{ML_text "foo"} is 
+  It is also possible to redirect the ``channel'' where the string @{ML_text "foo"} is 
   printed to a separate file, e.g. to prevent Proof General from choking on massive 
   amounts of trace output. This redirection can be achieved using the code
 *}
@@ -152,8 +152,11 @@
 
   In a similar way you can use antiquotations to refer to theorems or simpsets:
 
-  @{ML [display] "@{thm allI}"}
-  @{ML [display] "@{simpset}"}
+  @{ML_response_fake [display] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
+  @{ML_response_fake [display] "@{simpset}" "\<dots>"}
+
+  (FIXME: what does a simpset look like? It seems to be the same problem
+  like tokens.)
 
   While antiquotations have many applications, they were originally introduced to 
   avoid explicit bindings for theorems such as
@@ -241,7 +244,7 @@
 
   \begin{readmore}
   Types are described in detail in \isccite{sec:types}. Their
-  definition and many useful operations can be found in @{ML_file "Pure/type.ML"}.
+  definition and many useful operations can also be found in @{ML_file "Pure/type.ML"}.
   \end{readmore}
 *}
 
@@ -350,7 +353,7 @@
   
   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.
+  term is well-formed, or type-checks, relative to a theory.
   Type-checking is done via the function @{ML cterm_of}, which converts 
   a @{ML_type term} into a  @{ML_type cterm}, a \emph{certified} term. 
   Unlike @{ML_type term}s, which are just trees, @{ML_type
@@ -358,7 +361,7 @@
   type-correct, and that can only be constructed via the ``official
   interfaces''.
 
-  Type checking is always relative to a theory context. For now we use
+  Type-checking is always relative to a theory context. For now we use
   the @{ML "@{theory}"} antiquotation to get hold of the current theory.
   For example we can write
 
@@ -368,7 +371,11 @@
 
   @{ML_response_fake [display] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"}
 
-  A slightly more elaborate example is
+  Attempting
+
+  @{ML_response_fake_both [display] "@{cterm \"1 + True\"}" "Type unification failed \<dots>"}
+
+  yields an error. A slightly more elaborate example is
 
 @{ML_response_fake [display] 
 "let
@@ -391,8 +398,8 @@
 
 text {*
   Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm} 
-  that can only be built by going through interfaces, which means that all your proofs 
-  will be checked. 
+  that can only be built by going through interfaces. In effect all proofs 
+  are checked. 
 
   To see theorems in ``action'', let us give a proof for the following statement
 *}
@@ -472,7 +479,8 @@
   prop"} is just the identity function and used as a syntactic marker. 
   
   \begin{readmore}
-  For more on goals see \isccite{sec:tactical-goals}. 
+  For more on goals see \isccite{sec:tactical-goals}. (FIXME: in which
+  file is most code for dealing with goals?)
   \end{readmore}
 
   Tactics are functions that map a goal state to a (lazy)
@@ -525,7 +533,8 @@
 end" "?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P"}
 
   \begin{readmore}
-  To learn more about the function @{ML Goal.prove} see \isccite{sec:results}.
+  To learn more about the function @{ML Goal.prove} see \isccite{sec:results} and
+  the file @{ML_file "Pure/goal.ML"}.
   \end{readmore}