# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1233124156 0
# Node ID fdb9ea86c2a3263325a846dc86a452617ba037ff
# Parent  b02904872d6b2af4b880e376d641a520c37c348e
polished

diff -r b02904872d6b -r fdb9ea86c2a3 CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Tue Jan 27 21:22:27 2009 +0000
+++ b/CookBook/FirstSteps.thy	Wed Jan 28 06:29:16 2009 +0000
@@ -381,6 +381,8 @@
   number representing their sum.
   \end{exercise}
 
+
+  (FIXME: operation from page 19 of the implementation manual)
 *}
 
 section {* Type-Checking *}
@@ -429,6 +431,8 @@
   result that type-checks.
   \end{exercise}
 
+  (FIXME: @{text "ctyp_of"})
+
 *}
 
 section {* Theorems *}
@@ -503,6 +507,8 @@
 text {*
 
 @{ML_response [display] "Sign.base_name \"List.list.Nil\"" "\"Nil\""}
+
+  authentic syntax
   
 *}
 
@@ -531,7 +537,7 @@
 
 text {*
   @{ML K} ``wraps'' a function around the argument @{text "x"}. However, this 
-  function ignores its argument. So @{ML K} defines a constant function 
+  function ignores its argument. As a result @{ML K} defines a constant function 
   returning @{text x}.
 
   The next combinator is reverse application, @{ML "|>"}, defined as 
@@ -585,7 +591,7 @@
   (FIXME: give a real world example involving theories)
 
   Similarly, the combinator @{ML "#>"} is the reverse function 
-  composition. It can be used to define functions as follows
+  composition. It can be used to define the following function
 *}
 
 ML{*val inc_by_six = 
@@ -660,11 +666,11 @@
         |-> (fn x => fn y => x + y)*}
 
 text {*
-  Recall that @{ML "|>"} is the reverse function applications. The related 
-  reverse function composition is @{ML "#>"}. In fact all combinators @{ML "|->"},
+  Recall that @{ML "|>"} is the reverse function applications. Recall also that the related 
+  reverse function composition is @{ML "#>"}. In fact all the combinators @{ML "|->"},
   @{ML "|>>"} and @{ML "||>"} described above have related combinators for function
-  composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "|->"}, 
-  the function @{text double} can also be written as
+  composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "#->"}, 
+  for example, the function @{text double} can also be written as
 *}
 
 ML{*val double =
diff -r b02904872d6b -r fdb9ea86c2a3 CookBook/Parsing.thy
--- a/CookBook/Parsing.thy	Tue Jan 27 21:22:27 2009 +0000
+++ b/CookBook/Parsing.thy	Wed Jan 28 06:29:16 2009 +0000
@@ -584,7 +584,7 @@
 
   The option @{text "-k foobar"} indicates which postfix the name of the keyword file 
   will be assigned. In the case above the file will be named @{text
-  "isar-keywords-foobar.el"}. As can be seen, this command requires log files to be
+  "isar-keywords-foobar.el"}. This command requires log files to be
   present (in order to extract the keywords from them). To generate these log
   files, we first package the code above into a separate theory file named
   @{text "Command.thy"}, say---see Figure~\ref{fig:commandtheory} for the
@@ -683,9 +683,9 @@
    $ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral.gz,HOL-FoobarCommand.gz}"}
 
   The result is the file @{text "isar-keywords-foobar.el"}. It should contain
-  the string @{text "foobar"} twice (to see whether things went wrong, check
+  the string @{text "foobar"} twice.\footnote{To see whether things are fine, check
   that @{text "grep foobar"} on this file returns something
-  non-empty).  This keyword file needs to
+  non-empty.}  This keyword file needs to
   be copied into the directory @{text "~/.isabelle/etc"}. To make Isabelle
   aware of this keyword file, we have to start Isabelle with the option @{text
   "-k foobar"}, i.e.
@@ -740,7 +740,7 @@
   \isacommand{definition} and \isacommand{declare}.  In other cases,
   commands are expected to parse some arguments, for example a proposition,
   and then ``open up'' a proof in order to prove the proposition (for example
-  \isacommand{lemma}) or prove some other properties (for example in
+  \isacommand{lemma}) or prove some other properties (for example
   \isacommand{function}). To achieve this kind of behaviour, we have to use the kind
   indicator @{ML thy_goal in OuterKeyword}.
 
@@ -767,7 +767,7 @@
 end *}
 
 text {*
-  The function @{text set_up_thm} takes a string (the proposition to be
+  The function @{text set_up_thm} in Lines 2 to 7 takes a string (the proposition to be
   proved) and a context.  The context is necessary in order to be able to use
   @{ML Syntax.read_prop}, which converts a string into a proper proposition.
   In Line 6 the function @{ML Proof.theorem_i} starts the proof for the
@@ -794,6 +794,8 @@
   \isacommand{done}
   \end{isabelle}
 
+  Similarly for the other function composition combinators.
+
   
   (FIXME What does @{text "Toplevel.theory"} @{text "Toplevel.print"}?)
 
diff -r b02904872d6b -r fdb9ea86c2a3 cookbook.pdf
Binary file cookbook.pdf has changed