--- a/CookBook/FirstSteps.thy	Thu Oct 30 13:36:51 2008 +0100
+++ b/CookBook/FirstSteps.thy	Sat Nov 01 15:20:36 2008 +0100
@@ -329,8 +329,6 @@
 
 section {* Type Checking *}
 
-ML {* cterm_of @{theory} @{term "a + b = c"} *}
-
 text {* 
   
   We can freely construct and manipulate terms, since they are just
@@ -409,7 +407,7 @@
   Qt 
   |> implies_intr assm2
   |> implies_intr assm1
-end" "(FIXME)"}
+end" "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
 
   This code-snippet constructs the following proof:
 
@@ -489,7 +487,6 @@
 apply assumption
 done
 
-
 text {*
   To start the proof, the function  @{ML "Goal.prove"}~@{text "ctxt xs As C tac"} sets 
   up a goal state for proving the goal @{text C} under the assumptions @{text As} 
@@ -509,7 +506,7 @@
     THEN assume_tac 1
     THEN resolve_tac [disjI1] 1
     THEN assume_tac 1)
-end" "(FIXME)"}
+end" "?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P"}
 
   \begin{readmore}
   To learn more about the function @{ML Goal.prove} see \isccite{sec:results}.
@@ -529,7 +526,7 @@
     THEN' assume_tac 
     THEN' resolve_tac [disjI1] 
     THEN' assume_tac) 1)
-end" "(FIXME)"}
+end" "?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P"}
 
   (FIXME: are there any advantages/disadvantages about this way?) 
 *}

--- a/CookBook/Parsing.thy	Thu Oct 30 13:36:51 2008 +0100
+++ b/CookBook/Parsing.thy	Sat Nov 01 15:20:36 2008 +0100
@@ -213,9 +213,7 @@
   Note that @{ML "Scan.repeat"} stores the parsed items in a list. The function
   @{ML "Scan.repeat1"} is similar, but requires that the parser @{ML_text "p"} 
   succeeds at least once.
-*}
- 
-text {* 
+
   After parsing succeeded, one nearly always wants to apply a function on the parsed 
   items. This is done using the function @{ML_open "(p >> f)" for p f} which runs 
   first the parser @{ML_text p} and upon successful completion applies the 
@@ -273,14 +271,16 @@
 
   produces three tokens where the first and the last are identifiers, since 
   @{ML_text [quotes] "hello"} and @{ML_text [quotes] "world"} do not match 
-  any other category. The second indicates a space. If we parse
+  any other category. The second indicates a space. Many parsing functions 
+  later on will require spaces, comments and the like to have been filtered out.
+  If we parse
 
 @{ML_response [display] "OuterSyntax.scan Position.none \"inductive|for\"" 
 "[OuterLex.Token (\<dots>,(OuterLex.Command, \"inductive\"),\<dots>), 
  OuterLex.Token (\<dots>,(OuterLex.Keyword, \"|\"),\<dots>), 
  OuterLex.Token (\<dots>,(OuterLex.Keyword, \"for\"),\<dots>)]"}
 
-  we obtain a list of command and keyword tokens.
+  we obtain a list consiting of only command and keyword tokens.
   If you want to see which keywords and commands are currently known, use
   the following (you might have to adjust the @{ML print_depth} in order to
   see the complete list):
@@ -305,7 +305,6 @@
 "((\"where\",\<dots>),(\"|\",\<dots>))"}
 
   Like before, we can sequentially connect parsers with @{ML "(op --)"}. For example 
-  follows
 
 @{ML_response [display]
 "let 
@@ -316,7 +315,7 @@
 "((\"|\",\"in\"),[])"}
 
   The parser @{ML_open "OuterParse.enum s p" for s p} parses a possibly empty 
-  list of items recognized by the parser @{ML_text p}, where the items are 
+  list of items recognised by the parser @{ML_text p}, where the items are 
   separated by @{ML_text s}. For example
 
 @{ML_response [display]
@@ -329,7 +328,7 @@
 
   Note that we had to add a @{ML_text [quotes] "\\n"} at the end of the parsed
   string, otherwise the parser would have consumed all tokens and then failed with
-  the exception @{ML_text "FAIL"}. @{ML "OuterParse.enum1"} works similarly, 
+  the exception @{ML_text "MORE"}. @{ML "OuterParse.enum1"} works similarly, 
   except that the parsed list must be non-empty.
 
 *}

--- a/CookBook/Recipes/NamedThms.thy	Thu Oct 30 13:36:51 2008 +0100
+++ b/CookBook/Recipes/NamedThms.thy	Sat Nov 01 15:20:36 2008 +0100
@@ -41,6 +41,7 @@
 
 lemma rule1[foo]: "A" sorry
 lemma rule2[foo]: "B" sorry
+lemma rule3[foo]: "C" sorry
 
 text {* undeclare them: *}
 
@@ -54,7 +55,7 @@
   In an ML-context the rules marked with @{ML_text "foo"} an be retrieved
   using
 
-  @{ML_response_fake [display] "FooRules.get @{context}" "(FIXME)"}
+  @{ML_response_fake [display] "FooRules.get @{context}" "[\"?C\",\"?B\"]"}
 
   \begin{readmore}
   For more information see @{ML_file "Pure/Tools/named_thms.ML"}.

Binary file cookbook.pdf has changed