--- a/CookBook/FirstSteps.thy	Tue Mar 17 12:26:34 2009 +0100
+++ b/CookBook/FirstSteps.thy	Tue Mar 17 17:32:12 2009 +0100
@@ -261,19 +261,27 @@
        |> (curry list_comb) pred *}
 
 text {*
-  The point of this code is to extract the argument types of the given
+  This code extracts the argument types of the given
   predicate and then generate for each type a distinct variable; finally it
-  applies the generated variables to the predicate. You can read this off from
-  how the function is coded: in Line 2, the function @{ML fastype_of}
-  calculates the type of the predicate; in Line 3, @{ML binder_types} produces
-  the list of argument types; Line 4 pairs up each type with the string (or name)
-  @{text "z"}; the function @{ML variant_frees in Variable} generates for each
-  @{text "z"} a unique name avoiding @{text pred}; the list of name-type pairs
-  is turned into a list of variable terms in Line 6, which in the last line
-  are applied by the function @{ML list_comb} to the predicate. We have to use
-  the function @{ML curry}, because @{ML list_comb} expects the predicate and
-  the argument list as a pair.
+  applies the generated variables to the predicate. For example
+
+  @{ML_response_fake [display,gray]
+"apply_fresh_args @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"} @{context} 
+ |> Syntax.string_of_term @{context}
+ |> warning"
+  "P z za zb"}
 
+  You can read this off this behaviour from how @{ML apply_fresh_args} is
+  coded: in Line 2, the function @{ML fastype_of} calculates the type of the
+  predicate; in Line 3, @{ML binder_types} produces the list of argument
+  types (in the case above the list @{text "[nat, int, unit]"}); Line 4 pairs up each 
+  type with the string  @{text "z"}; the
+  function @{ML variant_frees in Variable} generates for each @{text "z"} a
+  unique name avoiding @{text pred}; the list of name-type pairs is turned
+  into a list of variable terms in Line 6, which in the last line are applied
+  by the function @{ML list_comb} to the predicate. We have to use the
+  function @{ML curry}, because @{ML list_comb} expects the predicate and the
+  argument list as a pair.
   
   The combinator @{ML "#>"} is the reverse function composition. It can be
   used to define the following function
@@ -463,6 +471,10 @@
   kinds of logical elements from th ML-level.
 *}
 
+text {*
+  (FIXME: say something about @{text "@{binding \<dots>}"}
+*}
+
 section {* Terms and Types *}
 
 text {*
@@ -584,6 +596,9 @@
     Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ 
                (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
 
+  (FIXME: handy functions for constructing terms @{ML list_comb}, @{ML lambda})
+
+
   Although types of terms can often be inferred, there are many
   situations where you need to construct types manually, especially  
   when defining constants. For example the function returning a function 

--- a/CookBook/Package/Ind_Code.thy	Tue Mar 17 12:26:34 2009 +0100
+++ b/CookBook/Package/Ind_Code.thy	Tue Mar 17 17:32:12 2009 +0100
@@ -4,8 +4,6 @@
 
 section {* Code *}
 
-subsection {* Definitions *}
-
 text {*
   @{text [display] "rule ::= \<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}
 
@@ -42,8 +40,8 @@
 
   @{text [display] "pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}
 
-  We use the following wrapper function to make the definition via
-  @{ML LocalTheory.define}. The function takes a predicate name, a syntax
+  In order to make definitions, we use the following wrapper for 
+  @{ML LocalTheory.define}. The wrapper takes a predicate name, a syntax
   annotation and a term representing the right-hand side of the definition.
 *}
 
@@ -56,15 +54,13 @@
 end*}
 
 text {*
-  It returns the definition (as theorem) and the local theory in which this definition has 
+  It returns the definition (as a theorem) and the local theory in which this definition has 
   been made. In Line 4 @{ML internalK in Thm} is just a flag attached to the 
-  theorem (others possibilities are @{ML definitionK in Thm} or @{ML axiomK in Thm}). 
+  theorem (others possibilities are @{ML definitionK in Thm} and @{ML axiomK in Thm}). 
   These flags just classify theorems and have no significant meaning, except 
-  for tools such as finding theorems in the theorem database. We also
+  for tools that, for example, find theorems in the theorem database. We also
   use @{ML empty_binding in Attrib} in Line 3, since the definition does 
-  not need any theorem attributes. Note the definition has not yet been 
-  stored in the theorem database. So at the moment we can only refer to it
-  via the return value. A testcase for this functions is
+  not need to have any theorem attributes. A testcase for this function is
 *}
 
 local_setup %gray {* fn lthy =>
@@ -76,23 +72,27 @@
 end *}
 
 text {*
-  which prints out the theorem @{prop "MyTrue \<equiv> True"}. Since we are
-  testing the function inside \isacommand{local\_setup} we have also
-  access to theorem associated with this definition.
+  which makes the difinition @{prop "MyTrue \<equiv> True"} and then prints it out. 
+  Since we are testing the function inside \isacommand{local\_setup}, i.e.~make
+  changes to the ambient theory, we can query the definition using the usual
+  command \isacommand{thm}:
 
   \begin{isabelle}
   \isacommand{thm}~@{text "MyTrue_def"}\\
   @{text "> MyTrue \<equiv> True"}
   \end{isabelle}
 
-  The next function constructs the term for the definition, namely 
+  The next two functions construct the terms we need for the definitions, namely 
+  terms of the form 
 
   @{text [display] "\<lambda>\<^raw:$zs$>. \<forall>preds. orules \<longrightarrow> pred \<^raw:$zs$>"}
 
-  The variables @{text "\<^raw:$zs$>"} need to be chosen so to not occur
-  in the @{text orules} and also be distinct from @{text "pred"}. The function
-  constructs the term for one particular predicate @{text "pred"}; the number
-  of @{text "\<^raw:$zs$>"} is determined by the nunber of types. 
+  The variables @{text "\<^raw:$zs$>"} need to be chosen so that they do not occur
+  in the @{text orules} and also be distinct from @{text "preds"}. 
+
+  The first function constructs the term for one particular predicate @{text
+  "pred"}; the number of arguments @{text "\<^raw:$zs$>"} of this predicate is
+  determined by the number of argument types of @{text "arg_tys"}.
 *}
 
 ML %linenosgray{*fun defs_aux lthy orules preds (pred, arg_tys) =
@@ -112,16 +112,17 @@
 end*}
 
 text {*
-  The code in Lines 5 to 9 produce the fresh @{text "\<^raw:$zs$>"} with which the 
-  predicate is applied. For this it pairs every type with a string @{text [quotes] "z"} 
-  (Line 7); then generates variants for all these strings (names) so that they are 
-  unique w.r.t.~to the orules and predicates; in Line 9 it generates the corresponding 
-  variable terms for the unique names.
+  The code in Lines 5 to 9 produce the fresh @{text "\<^raw:$zs$>"}. For this
+  it pairs every argument type with the string @{text [quotes] "z"} (Line 7);
+  then generates variants for all these strings so that they are unique
+  w.r.t.~to the @{text "orules"} and the predicates; in Line 9 it generates the
+  corresponding variable terms for the unique strings.
 
-  The unique free variables are applied to the predicate (Line 11); then
-  the @{text orules} are prefixed (Line 12); in Line 13 we
-  quantify over all predicates; and in line 14 we just abstract over all
-  the (fresh)  @{text "\<^raw:$zs$>"}, i.e.~the arguments of the predicate.
+  The unique free variables are applied to the predicate (Line 11) using the
+  function @{ML list_comb}; then the @{text orules} are prefixed (Line 12); in
+  Line 13 we quantify over all predicates; and in line 14 we just abstract
+  over all the @{text "\<^raw:$zs$>"}, i.e.~the fresh arguments of the
+  predicate.
 
   A testcase for this function is
 *}
@@ -140,16 +141,15 @@
 end *}
 
 text {*
-  It constructs the term for the predicate @{term "even"}. So we obtain as printout
-  the term
+  It constructs the left-hand side for the definition of @{term "even"}. So we obtain 
+  as printout the term
 
   @{text [display] 
 "\<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n)) 
                          \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> even z"}
 
   The main function for the definitions now has to just iterate
-  the function @{ML defs_aux} over all predicates. THis is what the
-  next function does. 
+  the function @{ML defs_aux} over all predicates. 
 *}
 
 ML %linenosgray{*fun definitions rules preds prednames syns arg_typss lthy =
@@ -162,14 +162,19 @@
 end*}
 
 text {*
-  The argument @{text "preds"} is the list of predicates as @{ML_type term}s;
+  The argument @{text "preds"} is again the the list of predicates as 
+  @{ML_type term}s;
   the argument @{text "prednames"} is the list of names of the predicates;
-  @{text "arg_tyss"} is the list of argument-type-lists. 
+  @{text "arg_tyss"} is the list of argument-type-lists for each predicate. 
   
-  In line 4 we generate the intro rules in the object logic; for this we have to 
-  obtain the theory behind the local theory (Line 3); with this we can
-  call @{ML defs_aux} to generate the terms for the left-hand sides.
-  The actual definitions are made in Line 7.
+  The user give the introduction rules using meta-implications and meta-quantifications.
+  In line 4 we transform the introduction rules into the object logic (definitions
+  cannot use them). To do the transformation we have to 
+  obtain the theory behind the local theory (Line 3); with this theory 
+  we can use the function @{ML ObjectLogic.atomize_term} to make the
+  transformation (Line 4). The call to @{ML defs_aux} in Line 5 produces all
+  left-hand sides of the definitions. The actual definitions are then made in Line 7.
+  As the result we obtain a list of theorems and a local theory. 
 
   A testcase for this function is 
 *}
@@ -185,29 +190,31 @@
   val arg_tyss = [[@{typ "nat"}], [@{typ "nat"}]]
   val (defs, lthy') = definitions rules preds prednames syns arg_tyss lthy
 in
-  warning (str_of_thms lthy' defs); lthy
+  warning (str_of_thms lthy' defs); lthy'
 end *}
 
 text {*
 
-  It prints out the two definitions
+  \begin{isabelle}
+  \isacommand{thm}~@{text "even_def odd_def"}\\
+  @{text [break]
+"> even \<equiv> \<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n)) 
+>                                 \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> even z,
+> odd \<equiv> \<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n)) 
+>                                 \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> odd z"}
+  \end{isabelle}
 
-  @{text [display] 
-"even \<equiv> \<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n)) 
-                                \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> even z, 
- odd \<equiv> \<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n)) 
-                                \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> odd z"}
 
   This completes the code concerning the definitions. Next comes the code for
   the induction principles. 
 
-  Recall the proof for the induction principle for @{term "even"}: 
+  Let us now turn to the induction principles. Recall that the proof of the 
+  induction principle for @{term "even"} was:
 *}
 
 lemma 
-  assumes prems: "even n"
-  shows "P 0 \<Longrightarrow> 
-             (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
+assumes prems: "even n"
+shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
 apply(atomize (full))
 apply(cut_tac prems)
 apply(unfold even_def)
@@ -217,27 +224,34 @@
 done
 
 text {* 
-  To automate this proof we need to be able to instantiate universal 
-  quantifiers. For this we use the following helper function. It
-  instantiates the @{text "?x"} in @{thm spec} with a @{ML_type cterm}.
+  We have to implement code that constructs the induction principle and then
+  a tactic that automatically proves it. 
+  
+  The tactic will use the following helper function for instantiating universal 
+  quantifiers. This function instantiates the @{text "?x"} in the theorem 
+  @{thm spec} with a given @{ML_type cterm}.
 *}
 
 ML{*fun inst_spec ctrm = 
  Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}*}
 
 text {*
-  For example we can use it to instantiate an assumption:
+  For example we can use it in the following proof to instantiate the 
+  three quantifiers in the assumption. We use the tactic
 *}
 
+ML{*fun inst_spec_tac ctrms = 
+  EVERY' (map (dtac o inst_spec) ctrms)*}
+
+text {*
+  and then apply use it with the @{ML_type cterm}s @{text "y1\<dots>y3"}. 
+  *}
+
 lemma "\<forall>(x1::nat) (x2::nat) (x3::nat). P x1 x2 x3 \<Longrightarrow> True"
 apply (tactic {* 
-  let 
-    val ctrms = [@{cterm "y1::nat"},@{cterm "y2::nat"},@{cterm "y3::nat"}]
-  in 
-    EVERY1 (map (dtac o inst_spec) ctrms)
-  end *})
+  inst_spec_tac  [@{cterm "y1::nat"},@{cterm "y2::nat"},@{cterm "y3::nat"}] 1 *})
 txt {* 
-  where it produces the goal state
+  We obtain the goal state
 
   \begin{minipage}{\textwidth}
   @{subgoals} 
@@ -245,15 +259,15 @@
 (*<*)oops(*>*)
 
 text {*
-  Now the tactic for proving the induction rules can be implemented 
-  as follows
+  Now the complete tactic for proving the induction principles can 
+  be implemented as follows:
 *}
 
 ML %linenosgray{*fun induction_tac defs prems insts =
   EVERY1 [ObjectLogic.full_atomize_tac,
           cut_facts_tac prems,
           K (rewrite_goals_tac defs),
-          EVERY' (map (dtac o inst_spec) insts),
+          inst_spec_tac insts,
           assume_tac]*}
 
 text {*
@@ -261,43 +275,47 @@
   A testcase for the tactic is
 *}
 
+ML{*fun test_tac prems = 
+let
+  val defs = [@{thm even_def}, @{thm odd_def}]
+  val insts = [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}]
+in 
+  induction_tac defs prems insts 
+end*}
+
+text {*
+  which indeed proves the induction principle. 
+*}
+
 lemma 
-  assumes prems: "even n"
-  shows "P 0 \<Longrightarrow> 
-           (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
-apply(tactic {* 
-  let
-     val defs = [@{thm even_def}, @{thm odd_def}]
-     val insts = [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}]
-  in 
-    induction_tac defs @{thms prems} insts 
-  end *})
+assumes prems: "even n"
+shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
+apply(tactic {* test_tac @{thms prems} *})
 done
 
-
 text {*
-  which indeed proves the lemma. 
-
   While the generic proof for the induction principle is relatively simple, 
-  it is a bit harder to set up the goals just from the given introduction 
-  rules. For this we have to construct for each predicate @{text "pred"}
+  it is a bit harder to construct the goals from just the introduction 
+  rules the user states. In general we have to construct for each predicate 
+  @{text "pred"} a goal of the form
 
   @{text [display] 
   "\<And>\<^raw:$zs$>. pred \<^raw:$zs$> \<Longrightarrow> rules[preds := \<^raw:$Ps$>] \<Longrightarrow> \<^raw:$P$>\<^raw:$zs$>"}
 
-  where the given predicates @{text preds} are replaced by new distinct 
-  ones written as @{text "\<^raw:$Ps$>"}, and also need to be applied to
-  new variables @{text "\<^raw:$zs$>"}. 
+  where the given predicates @{text preds} are replaced in the introduction 
+  rule @{text "rules"} by new distinct variables written as @{text "\<^raw:$Ps$>"}. 
+  We also need to generate fresh arguments for the predicate @{text "pred"} and
+  the @{text "\<^raw:$P$>"} in the conclusion of the induction principle.
 
   The function below expects that the rules are already appropriately
-  replaced. The argument @{text "mrules"} stands for these modified
+  substitued. The argument @{text "srules"} stands for these substituted
   introduction rules; @{text cnewpreds} are the certified terms coresponding
   to the variables @{text "\<^raw:$Ps$>"}; @{text "pred"} is the predicate for
   which we prove the introduction principle; @{text "newpred"} is its
-  replacement and @{text "tys"} are the types of its argument.
+  replacement and @{text "tys"} are the argument types of this predicate.
 *}
 
-ML %linenosgray{* fun prove_induction lthy defs mrules cnewpreds ((pred, newpred), tys)  =
+ML %linenosgray{*fun prove_induction lthy defs srules cnewpreds ((pred, newpred), tys)  =
 let
   val zs = replicate (length tys) "z"
   val (newargnames, lthy') = Variable.variant_fixes zs lthy;
@@ -305,7 +323,7 @@
   
   val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs))
   val goal = Logic.list_implies 
-         (mrules, HOLogic.mk_Trueprop (list_comb (newpred, newargs)))
+         (srules, HOLogic.mk_Trueprop (list_comb (newpred, newargs)))
 in
   Goal.prove lthy' [] [prem] goal
   (fn {prems, ...} => induction_tac defs prems cnewpreds)
@@ -313,31 +331,37 @@
 end *}
 
 text {* 
-  In Line 3 we produce a list of names @{text "\<^raw:$zs$>"} according to the type 
-  list. Line 4 makes these names unique and declare them as \emph{free} (but fixed)
-  variables. These variables are free in the new theory @{text "lthy'"}. In Line 5
-  we just construct the terms corresponding to the variables. The term variables are
-  applied to the predicate in Line 7 (this is the first premise 
-  @{text "pred \<^raw:$zs$>"} of the induction principle). In Line 8 and 9
-  we first the term  @{text "\<^raw:$P$>\<^raw:$zs$>"} and then add
-  the (modified) introduction rules as premises.
+  In Line 3 we produce a name @{text "\<^raw:$zs$>"} for each type in the 
+  argument type list. Line 4 makes these names unique and declares them as 
+  \emph{free} (but fixed) variables in the local theory @{text "lthy'"}. In 
+  Line 5 we just construct the terms corresponding to these variables. 
+  The term variables are applied to the predicate in Line 7 (this corresponds
+  to the first premise @{text "pred \<^raw:$zs$>"} of the induction principle). 
+  In Line 8 and 9, we first construct the term  @{text "\<^raw:$P$>\<^raw:$zs$>"} 
+  and then add the (modified) introduction rules as premises. In case that
+  no introduction rules are given, the conclusion of this implications needs
+  to be wrapped inside a @{term Trueprop}, otherwise the Isabelle's goal
+  mechanism will fail. 
 
-  In Line 11 we set up the goal to be proved; call the induction tactic in
-  Line 13. This returns a theorem. However, it is a theorem proved inside
-  the local theory @{text "lthy'"} where the variables @{text "\<^raw:$zs$>"} are
-  fixed, but free. By exporting this theorem from @{text "lthy'"} (which does contain
-  the  @{text "\<^raw:$zs$>"} as free) to @{text "lthy"} (which does not), we
-  obtain the desired quantifications @{text "\<And>\<^raw:$zs$>"}.
+  In Line 11 we set up the goal to be proved; then call the tactic for proving the 
+  induction principle. This tactic expects the (certified) predicates with which
+  the introduction rules have been substituted. This will return a theorem. 
+  However, it is a theorem proved inside the local theory @{text "lthy'"} where 
+  the variables @{text "\<^raw:$zs$>"} are fixed, but free. By exporting this 
+  theorem from @{text "lthy'"} (which contains the  @{text "\<^raw:$zs$>"} 
+  as free) to @{text "lthy"} (which does not), we obtain the desired quantifications 
+  @{text "\<And>\<^raw:$zs$>"}.
 
-  So it is left to produce the modified rules and 
+  Now it is left to produce the new predicated with which the introduction
+  rules are substituted. 
 *}
 
-ML %linenosgray{*fun inductions rules defs preds tyss lthy1  =
+ML %linenosgray{*fun inductions rules defs preds tyss lthy  =
 let
   val Ps = replicate (length preds) "P"
-  val (newprednames, lthy2) = Variable.variant_fixes Ps lthy1
+  val (newprednames, lthy') = Variable.variant_fixes Ps lthy
   
-  val thy = ProofContext.theory_of lthy2
+  val thy = ProofContext.theory_of lthy'
 
   val tyss' = map (fn tys => tys ---> HOLogic.boolT) tyss
   val newpreds = map Free (newprednames ~~ tyss')
@@ -345,9 +369,9 @@
   val rules' = map (subst_free (preds ~~ newpreds)) rules
 
 in
-  map (prove_induction lthy2 defs rules' cnewpreds) 
+  map (prove_induction lthy' defs rules' cnewpreds) 
         (preds ~~ newpreds ~~ tyss)
-          |> ProofContext.export lthy2 lthy1
+          |> ProofContext.export lthy' lthy
 end*}
 
 ML {*
@@ -458,20 +482,10 @@
     |> snd
 end*}
 
-ML{*fun read_specification' vars specs lthy =
-let 
-  val specs' = map (fn (a, s) => (a, [s])) specs
-  val ((varst, specst), _) = 
-                   Specification.read_specification vars specs' lthy
-  val specst' = map (apsnd the_single) specst
-in   
-  (varst, specst')
-end*}
-
 ML{*fun add_inductive pred_specs rule_specs lthy =
 let
-  val (pred_specs', rule_specs') = 
-    read_specification' pred_specs rule_specs lthy
+  val ((pred_specs', rule_specs'), _) = 
+         Specification.read_spec pred_specs rule_specs lthy
 in
   add_inductive_i pred_specs' rule_specs' lthy
 end*} 

--- a/CookBook/Package/Ind_Interface.thy	Tue Mar 17 12:26:34 2009 +0100
+++ b/CookBook/Package/Ind_Interface.thy	Tue Mar 17 17:32:12 2009 +0100
@@ -179,17 +179,17 @@
   are not yet in any way reflected in the introduction rules. So the task of
   @{ML add_inductive in SimpleInductivePackage} is to transform the strings
   into properly typed terms. For this it can use the function 
-  @{ML read_specification in Specification}. This function takes some constants
+  @{ML read_spec in Specification}. This function takes some constants
   with possible typing annotations and some rule specifications and attempts to
   find a type according to the given type constraints and the type constraints
   by the surrounding (local theory). However this function is a bit
   too general for our purposes: we want that each introduction rule has only 
   name (for example @{text even0} or @{text evenS}), if a name is given at all.
-  The function @{ML read_specification in Specification} however allows more
+  The function @{ML read_spec in Specification} however allows more
   than one rule. Since it is quite convenient to rely on this function (instead of
   building your own) we just quick ly write a wrapper function that translates
   between our specific format and the general format expected by 
-  @{ML read_specification in Specification}. The code of this wrapper is as follows:
+  @{ML read_spec in Specification}. The code of this wrapper is as follows:
 
   @{ML_chunk [display,gray,linenos] read_specification}
 
@@ -287,22 +287,22 @@
 text {*
   During parsing, both predicates and parameters are treated as variables, so
   the lists \verb!preds_syn! and \verb!params_syn! are just appended
-  before being passed to @{ML read_specification in Specification}. Note that the format
-  for rules supported by @{ML read_specification in Specification} is more general than
+  before being passed to @{ML read_spec in Specification}. Note that the format
+  for rules supported by @{ML read_spec in Specification} is more general than
   what is required for our package. It allows several rules to be associated
   with one name, and the list of rules can be partitioned into several
   sublists. In order for the list \verb!intro_srcs! of introduction rules
-  to be acceptable as an input for @{ML read_specification in Specification}, we first
+  to be acceptable as an input for @{ML read_spec in Specification}, we first
   have to turn it into a list of singleton lists. This transformation
   has to be reversed later on by applying the function
   @{ML [display] "the_single: 'a list -> 'a"}
   to the list \verb!specs! containing the parsed introduction rules.
-  The function @{ML read_specification in Specification} also returns the list \verb!vars!
+  The function @{ML read_spec in Specification} also returns the list \verb!vars!
   of predicates and parameters that contains the inferred types as well.
   This list has to be chopped into the two lists \verb!preds_syn'! and
   \verb!params_syn'! for predicates and parameters, respectively.
   All variables occurring in a rule but not in the list of variables passed to
-  @{ML read_specification in Specification} will be bound by a meta-level universal
+  @{ML read_spec in Specification} will be bound by a meta-level universal
   quantifier.
 *}
 

--- a/CookBook/Parsing.thy	Tue Mar 17 12:26:34 2009 +0100
+++ b/CookBook/Parsing.thy	Tue Mar 17 17:32:12 2009 +0100
@@ -450,7 +450,7 @@
 in 
   (OuterParse.$$$ \"|\" -- OuterParse.$$$ \"in\") input
 end"
-"((\"|\", \"in\"),[])"}
+"((\"|\", \"in\"), [])"}
 
   The parser @{ML "OuterParse.enum s p" for s p} parses a possibly empty 
   list of items recognised by the parser @{text p}, where the items being parsed
@@ -462,7 +462,7 @@
 in 
   (OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input
 end" 
-"([\"in\", \"in\", \"in\"],[\<dots>])"}
+"([\"in\", \"in\", \"in\"], [\<dots>])"}
 
   @{ML "OuterParse.enum1"} works similarly, except that the parsed list must
   be non-empty. Note that we had to add a string @{text [quotes] "foo"} at the
@@ -479,7 +479,7 @@
   Scan.finite OuterLex.stopper 
          (OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input
 end" 
-"([\"in\", \"in\", \"in\"],[])"}
+"([\"in\", \"in\", \"in\"], [])"}
 
   The following function will help to run examples.
 

Binary file cookbook.pdf has changed