--- a/CookBook/FirstSteps.thy	Thu Feb 19 01:09:16 2009 +0000
+++ b/CookBook/FirstSteps.thy	Thu Feb 19 14:44:53 2009 +0000
@@ -62,7 +62,7 @@
   
 *}
 
-section {* Debugging and Printing *}
+section {* Debugging and Printing\label{sec:printing} *}
 
 text {*
 
@@ -118,9 +118,230 @@
 "Exception- ERROR \"foo\" raised
 At command \"ML\"."}
 
-  Section~\ref{sec:printing} will give more information about printing 
-  the main data structures of Isabelle, namely @{ML_type term}, @{ML_type cterm} 
-  and @{ML_type thm}.
+  Most often you want to inspect data of type @{ML_type term}, @{ML_type cterm} 
+  or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing them, 
+  but  for quick-and-dirty solutions they are far too unwieldy. A simple way to transform 
+  a term into a string is to use the function @{ML Syntax.string_of_term}.
+
+  @{ML_response_fake [display,gray]
+  "Syntax.string_of_term @{context} @{term \"1::nat\"}"
+  "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""}
+
+  This produces a string with some additional information encoded in it. The string
+  can be properly printed by using the function @{ML warning}.
+
+  @{ML_response_fake [display,gray]
+  "warning (Syntax.string_of_term @{context} @{term \"1::nat\"})"
+  "\"1\""}
+
+  A @{ML_type cterm} can be transformed into a string by the following function.
+*}
+
+ML{*fun str_of_cterm ctxt t =  
+   Syntax.string_of_term ctxt (term_of t)*}
+
+text {*
+  If there are more than one @{ML_type cterm}s to be printed, you can use the 
+  function @{ML commas} to separate them.
+*} 
+
+ML{*fun str_of_cterms ctxt ts =  
+   commas (map (str_of_cterm ctxt) ts)*}
+
+text {*
+  The easiest way to get the string of a theorem is to transform it
+  into a @{ML_type cterm} using the function @{ML crep_thm}.
+*}
+
+ML{*fun str_of_thm ctxt thm =
+  let
+    val {prop, ...} = crep_thm thm
+  in 
+    str_of_cterm ctxt prop
+  end*}
+
+text {* 
+  Again the function @{ML commas} helps with printing more than one theorem. 
+*}
+
+ML{*fun str_of_thms ctxt thms =  
+  commas (map (str_of_thm ctxt) thms)*}
+
+
+section {* Combinators\label{sec:combinators} *}
+
+text {*
+  (FIXME: maybe move before antiquotation section)
+
+  For beginners, perhaps the most puzzling parts in the existing code of Isabelle are
+  the combinators. At first they seem to greatly obstruct the
+  comprehension of the code, but after getting familiar with them, they
+  actually ease the understanding and also the programming.
+
+  \begin{readmore}
+  The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"}
+  and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans} 
+  contains further information about combinators.
+  \end{readmore}
+
+  The simplest combinator is @{ML I}, which is just the identity function defined as
+*}
+
+ML{*fun I x = x*}
+
+text {* Another simple combinator is @{ML K}, defined as *}
+
+ML{*fun K x = fn _ => x*}
+
+text {*
+  @{ML K} ``wraps'' a function around the argument @{text "x"}. However, this 
+  function ignores its argument. As a result, @{ML K} defines a constant function 
+  always returning @{text x}.
+
+  The next combinator is reverse application, @{ML "|>"}, defined as: 
+*}
+
+ML{*fun x |> f = f x*}
+
+text {* While just syntactic sugar for the usual function application,
+  the purpose of this combinator is to implement functions in a  
+  ``waterfall fashion''. Consider for example the function *}
+
+ML %linenosgray{*fun inc_by_five x =
+  x |> (fn x => x + 1)
+    |> (fn x => (x, x))
+    |> fst
+    |> (fn x => x + 4)*}
+
+text {*
+  which increments its argument @{text x} by 5. It does this by first incrementing 
+  the argument by 1 (Line 2); then storing the result in a pair (Line 3); taking 
+  the first component of the pair (Line 4) and finally incrementing the first 
+  component by 4 (Line 5). This kind of cascading manipulations of values is quite
+  common when dealing with theories (for example by adding a definition, followed by
+  lemmas and so on). The reverse application allows you to read what happens in 
+  a top-down manner. This kind of coding should also be familiar, 
+  if you used Haskell's do-notation. Writing the function @{ML inc_by_five} using 
+  the reverse application is much clearer than writing
+*}
+
+ML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*}
+
+text {* or *}
+
+ML{*fun inc_by_five x = 
+       ((fn x => x + 4) o fst o (fn x => (x, x)) o (fn x => x + 1)) x*}
+
+text {* and typographically more economical than *}
+
+ML{*fun inc_by_five x =
+   let val y1 = x + 1
+       val y2 = (y1, y1)
+       val y3 = fst y2
+       val y4 = y3 + 4
+   in y4 end*}
+
+text {* 
+  Another reason why the let-bindings in the code above are better to be
+  avoided: it is more than easy to get the intermediate values wrong, not to 
+  mention the nightmares the maintenance of this code causes!
+
+
+  (FIXME: give a real world example involving theories)
+
+  Similarly, the combinator @{ML "#>"} is the reverse function 
+  composition. It can be used to define the following function
+*}
+
+ML{*val inc_by_six = 
+      (fn x => x + 1)
+   #> (fn x => x + 2)
+   #> (fn x => x + 3)*}
+
+text {* 
+  which is the function composed of first the increment-by-one function and then
+  increment-by-two, followed by increment-by-three. Again, the reverse function 
+  composition allows you to read the code top-down.
+
+  The remaining combinators described in this section add convenience for the
+  ``waterfall method'' of writing functions. The combinator @{ML tap} allows
+  you to get hold of an intermediate result (to do some side-calculations for
+  instance). The function
+
+ *}
+
+ML %linenosgray{*fun inc_by_three x =
+     x |> (fn x => x + 1)
+       |> tap (fn x => tracing (makestring x))
+       |> (fn x => x + 2)*}
+
+text {* 
+  increments the argument first by @{text "1"} and then by @{text "2"}. In the
+  middle (Line 3), however, it uses @{ML tap} for printing the ``plus-one''
+  intermediate result inside the tracing buffer. The function @{ML tap} can
+  only be used for side-calculations, because any value that is computed
+  cannot be merged back into the ``main waterfall''. To do this, you can use
+  the next combinator.
+
+  The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value
+  and returns the result together with the value (as a pair). For example
+  the function 
+*}
+
+ML{*fun inc_as_pair x =
+     x |> `(fn x => x + 1)
+       |> (fn (x, y) => (x, y + 1))*}
+
+text {*
+  takes @{text x} as argument, and then increments @{text x}, but also keeps
+  @{text x}. The intermediate result is therefore the pair @{ML "(x + 1, x)"
+  for x}. After that, the function increments the right-hand component of the
+  pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}.
+
+  The combinators @{ML "|>>"} and @{ML "||>"} are defined for 
+  functions manipulating pairs. The first applies the function to
+  the first component of the pair, defined as
+*}
+
+ML{*fun (x, y) |>> f = (f x, y)*}
+
+text {*
+  and the second combinator to the second component, defined as
+*}
+
+ML{*fun (x, y) ||> f = (x, f y)*}
+
+text {*
+  With the combinator @{ML "|->"} you can re-combine the elements from a pair.
+  This combinator is defined as
+*}
+
+ML{*fun (x, y) |-> f = f x y*}
+
+text {* and can be used to write the following roundabout version 
+  of the @{text double} function: 
+*}
+
+ML{*fun double x =
+      x |>  (fn x => (x, x))
+        |-> (fn x => fn y => x + y)*}
+
+text {*
+  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 "#->"}, 
+  for example, the function @{text double} can also be written as:
+*}
+
+ML{*val double =
+            (fn x => (x, x))
+        #-> (fn x => fn y => x + y)*}
+
+text {*
+  
+  (FIXME: find a good exercise for combinators)
+ 
 *}
 
 
@@ -212,7 +433,7 @@
   @{ML_response [display,gray] 
 "@{term \"(a::nat) + b = c\"}" 
 "Const (\"op =\", \<dots>) $ 
-                 (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
+   (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
 
   This will show the term @{term "(a::nat) + b = c"}, but printed using the internal
   representation of this term. This internal representation corresponds to the 
@@ -256,8 +477,9 @@
   inserting the invisible @{text "Trueprop"}-coercions whenever necessary. 
   Consider for example the pairs
 
-  @{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" "(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),
- Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}
+@{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" 
+"(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),
+  Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}
  
   where a coercion is inserted in the second component and 
 
@@ -445,7 +667,7 @@
   and @{text "(op *)"}:
 
   @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"op *\"})" 
-  "(Const (\"HOL.zero_class.zero\", \<dots>), 
+ "(Const (\"HOL.zero_class.zero\", \<dots>), 
  Const (\"HOL.times_class.times\", \<dots>))"}
 
   While you could use the complete name, for example 
@@ -471,7 +693,7 @@
   @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""}
 
   The difference between both functions is that @{ML extern_const in Sign} returns
-  the smallest name which is still unique, while @{ML base_name in Sign} always
+  the smallest name that is still unique, whereas @{ML base_name in Sign} always
   strips off all qualifiers.
 
   (FIXME authentic syntax on the ML-level)
@@ -567,13 +789,14 @@
 
   @{ML_response_fake [display,gray] 
 "let
-  val term = 
-   Const (@{const_name \"plus\"}, dummyT) $ @{term \"1::nat\"} $ Free (\"x\", dummyT)
+  val c = Const (@{const_name \"plus\"}, dummyT) 
+  val o = @{term \"1::nat\"} 
+  val v = Free (\"x\", dummyT)
 in   
-  Syntax.check_term @{context} term
+  Syntax.check_term @{context} (c $ o $ v)
 end"
-  "Const (\"HOL.plus_class.plus\", \"nat \<Rightarrow> nat \<Rightarrow> nat\") $
-       Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"}
+"Const (\"HOL.plus_class.plus\", \"nat \<Rightarrow> nat \<Rightarrow> nat\") $
+  Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"}
 
   Instead of giving explicitly the type for the constant @{text "plus"} and the free 
   variable @{text "x"}, the type-inference will fill in the missing information.
@@ -654,240 +877,36 @@
   (FIXME: how to add case-names to goal states)
 *}
 
-section {* Printing Terms and Theorems\label{sec:printing} *}
-
-text {* 
-  During development, you often want to inspect date of type @{ML_type term}, @{ML_type cterm} 
-  or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing them, 
-  but  for quick-and-dirty solutions they are far too unwieldy. A simple way to transform 
-  a term into a string is to use the function @{ML Syntax.string_of_term}.
-
-  @{ML_response_fake [display,gray]
-  "Syntax.string_of_term @{context} @{term \"1::nat\"}"
-  "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""}
-
-  This produces a string with some printing directions encoded in it. The string
-  can be properly printed by using the function @{ML warning}.
-
-  @{ML_response_fake [display,gray]
-  "warning (Syntax.string_of_term @{context} @{term \"1::nat\"})"
-  "\"1\""}
-
-  A @{ML_type cterm} can be transformed into a string by the following function.
-*}
-
-ML{*fun str_of_cterm ctxt t =  
-   Syntax.string_of_term ctxt (term_of t)*}
-
-text {*
-  If there are more than one @{ML_type cterm}s to be printed, you can use the 
-  function @{ML commas} to separate them.
-*} 
-
-ML{*fun str_of_cterms ctxt ts =  
-   commas (map (str_of_cterm ctxt) ts)*}
-
-text {*
-  The easiest way to get the string of a theorem is to transform it
-  into a @{ML_type cterm} using the function @{ML crep_thm}.
-*}
-
-ML{*fun str_of_thm ctxt thm =
-  let
-    val {prop, ...} = crep_thm thm
-  in 
-    str_of_cterm ctxt prop
-  end*}
-
-text {* 
-  Again the function @{ML commas} helps with printing more than one theorem. 
-*}
-
-ML{*fun str_of_thms ctxt thms =  
-  commas (map (str_of_thm ctxt) thms)*}
 
 section {* Theorem Attributes *}
 
 section {* Theories and Local Theories *}
 
+text {*
+  (FIXME: expand)
+
+  There are theories, proof contexts and local theories (in this order, if you
+  want to order them). 
+
+  In contrast to an ordinary theory, which simply consists of a type
+  signature, as well as tables for constants, axioms and theorems, a local
+  theory also contains additional context information, such as locally fixed
+  variables and local assumptions that may be used by the package. The type
+  @{ML_type local_theory} is identical to the type of \emph{proof contexts}
+  @{ML_type "Proof.context"}, although not every proof context constitutes a
+  valid local theory.
+
+ *}
+
+
+
 section {* Storing Theorems *}
 
 text {* @{ML PureThy.add_thms_dynamic} *}
 
 
-section {* Combinators\label{sec:combinators} *}
 
-text {*
-  For beginners, perhaps the most puzzling parts in the existing code of Isabelle are
-  the combinators. At first they seem to greatly obstruct the
-  comprehension of the code, but after getting familiar with them, they
-  actually ease the understanding and also the programming.
-
-  \begin{readmore}
-  The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"}
-  and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans} 
-  contains further information about combinators.
-  \end{readmore}
-
-  The simplest combinator is @{ML I}, which is just the identity function defined as
-*}
-
-ML{*fun I x = x*}
-
-text {* Another simple combinator is @{ML K}, defined as *}
-
-ML{*fun K x = fn _ => x*}
-
-text {*
-  @{ML K} ``wraps'' a function around the argument @{text "x"}. However, this 
-  function ignores its argument. As a result, @{ML K} defines a constant function 
-  always returning @{text x}.
-
-  The next combinator is reverse application, @{ML "|>"}, defined as: 
-*}
-
-ML{*fun x |> f = f x*}
-
-text {* While just syntactic sugar for the usual function application,
-  the purpose of this combinator is to implement functions in a  
-  ``waterfall fashion''. Consider for example the function *}
-
-ML %linenosgray{*fun inc_by_five x =
-  x |> (fn x => x + 1)
-    |> (fn x => (x, x))
-    |> fst
-    |> (fn x => x + 4)*}
-
-text {*
-  which increments its argument @{text x} by 5. It does this by first incrementing 
-  the argument by 1 (Line 2); then storing the result in a pair (Line 3); taking 
-  the first component of the pair (Line 4) and finally incrementing the first 
-  component by 4 (Line 5). This kind of cascading manipulations of values is quite
-  common when dealing with theories (for example by adding a definition, followed by
-  lemmas and so on). The reverse application allows you to read what happens in 
-  a top-down manner. This kind of coding should also be familiar, 
-  if you used Haskell's do-notation. Writing the function @{ML inc_by_five} using 
-  the reverse application is much clearer than writing
-*}
-
-ML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*}
-
-text {* or *}
-
-ML{*fun inc_by_five x = 
-       ((fn x => x + 4) o fst o (fn x => (x, x)) o (fn x => x + 1)) x*}
-
-text {* and typographically more economical than *}
-
-ML{*fun inc_by_five x =
-   let val y1 = x + 1
-       val y2 = (y1, y1)
-       val y3 = fst y2
-       val y4 = y3 + 4
-   in y4 end*}
-
-text {* 
-  Another reason why the let-bindings in the code above are better to be
-  avoided: it is more than easy to get the intermediate values wrong, not to 
-  mention the nightmares the maintenance of this code causes!
-
-
-  (FIXME: give a real world example involving theories)
-
-  Similarly, the combinator @{ML "#>"} is the reverse function 
-  composition. It can be used to define the following function
-*}
-
-ML{*val inc_by_six = 
-      (fn x => x + 1)
-   #> (fn x => x + 2)
-   #> (fn x => x + 3)*}
-
-text {* 
-  which is the function composed of first the increment-by-one function and then
-  increment-by-two, followed by increment-by-three. Again, the reverse function 
-  composition allows you to read the code top-down.
-
-  The remaining combinators described in this section add convenience for the
-  ``waterfall method'' of writing functions. The combinator @{ML tap} allows
-  you to get hold of an intermediate result (to do some side-calculations for
-  instance). The function
-
- *}
-
-ML %linenosgray{*fun inc_by_three x =
-     x |> (fn x => x + 1)
-       |> tap (fn x => tracing (makestring x))
-       |> (fn x => x + 2)*}
-
-text {* 
-  increments the argument first by @{text "1"} and then by @{text "2"}. In the
-  middle (Line 3), however, it uses @{ML tap} for printing the ``plus-one''
-  intermediate result inside the tracing buffer. The function @{ML tap} can
-  only be used for side-calculations, because any value that is computed
-  cannot be merged back into the ``main waterfall''. To do this, you can use
-  the next combinator.
-
-  The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value
-  and returns the result together with the value (as a pair). For example
-  the function 
-*}
-
-ML{*fun inc_as_pair x =
-     x |> `(fn x => x + 1)
-       |> (fn (x, y) => (x, y + 1))*}
-
-text {*
-  takes @{text x} as argument, and then increments @{text x}, but also keeps
-  @{text x}. The intermediate result is therefore the pair @{ML "(x + 1, x)"
-  for x}. After that, the function increments the right-hand component of the
-  pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}.
-
-  The combinators @{ML "|>>"} and @{ML "||>"} are defined for 
-  functions manipulating pairs. The first applies the function to
-  the first component of the pair, defined as
-*}
-
-ML{*fun (x, y) |>> f = (f x, y)*}
-
-text {*
-  and the second combinator to the second component, defined as
-*}
-
-ML{*fun (x, y) ||> f = (x, f y)*}
-
-text {*
-  With the combinator @{ML "|->"} you can re-combine the elements from a pair.
-  This combinator is defined as
-*}
-
-ML{*fun (x, y) |-> f = f x y*}
-
-text {* and can be used to write the following roundabout version 
-  of the @{text double} function: 
-*}
-
-ML{*fun double x =
-      x |>  (fn x => (x, x))
-        |-> (fn x => fn y => x + y)*}
-
-text {*
-  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 "#->"}, 
-  for example, the function @{text double} can also be written as:
-*}
-
-ML{*val double =
-            (fn x => (x, x))
-        #-> (fn x => fn y => x + y)*}
-
-text {*
-  
-  (FIXME: find a good exercise for combinators)
-*}
-
+(* FIXME: some code below *)
 
 (*<*)
 setup {*

--- a/CookBook/Intro.thy	Thu Feb 19 01:09:16 2009 +0000
+++ b/CookBook/Intro.thy	Thu Feb 19 14:44:53 2009 +0000
@@ -15,7 +15,7 @@
   against recent versions of Isabelle.  If something does not work, then
   please let us know. If you have comments, criticism or like to add to the
   tutorial, feel free---you are most welcome! The tutorial is meant to be 
-  gentle and comprehensive. To achieve this we need your feedback.
+  gentle and comprehensive. To achieve this we need your feedback. 
 *}
 
 section {* Intended Audience and Prior Knowledge *}

--- a/CookBook/Package/Ind_Interface.thy	Thu Feb 19 01:09:16 2009 +0000
+++ b/CookBook/Package/Ind_Interface.thy	Thu Feb 19 14:44:53 2009 +0000
@@ -245,15 +245,6 @@
   predicates, the names and types of their parameters, the actual introduction
   rules and a \emph{local theory}.  They return a local theory containing the
   definition and the induction principle as well introduction rules. 
-  
-  In contrast to an ordinary theory, which simply consists of a type
-  signature, as well as tables for constants, axioms and theorems, a local
-  theory also contains additional context information, such as locally fixed
-  variables and local assumptions that may be used by the package. The type
-  @{ML_type local_theory} is identical to the type of \emph{proof contexts}
-  @{ML_type "Proof.context"}, although not every proof context constitutes a
-  valid local theory.
-
 
   Note that @{ML add_inductive_i in SimpleInductivePackage} expects
   the types of the predicates and parameters to be specified using the

--- a/CookBook/Parsing.thy	Thu Feb 19 01:09:16 2009 +0000
+++ b/CookBook/Parsing.thy	Thu Feb 19 14:44:53 2009 +0000
@@ -527,7 +527,7 @@
   in which the @{text [quotes] "\\n"} causes the second token to be in 
   line 8.
 
-  Now by using the parser @{ML OuterParse.position} you can decode the positional
+  By using the parser @{ML OuterParse.position} you can decode the positional
   information and return it as part of the parsed input. For example
 
 @{ML_response_fake [display,gray]
@@ -563,7 +563,7 @@
   The function @{ML OuterParse.prop} is similar, except that it gives a different
   error message, when parsing fails. Looking closer at the result string you will
   have noticed that the parser not just returns the parsed string, but also some 
-  encoded positional information. You can see this better if you replace 
+  encoded information. You can see this better if you replace 
   @{ML Position.none} by @{ML "(Position.line 42)"}, say.
 
 @{ML_response [display,gray]
@@ -574,7 +574,7 @@
 end"
 "(\"\\^E\\^Ftoken\\^Fline=42\\^Fend_line=42\\^Efoo\\^E\\^F\\^E\", [])"}
   
-  The positional information is stored so that code called later will be
+  The positional information is stored so that code called later on will be
   able to give more precise error messages. 
 
 *}
@@ -606,18 +606,21 @@
 *}
 
 ML %linenosgray{*val spec_parser = 
-    OuterParse.opt_target --
-    OuterParse.fixes -- 
-    OuterParse.for_fixes --
-    Scan.optional 
-      (OuterParse.$$$ "where" |--
-         OuterParse.!!! 
-           (OuterParse.enum1 "|" 
-              (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}
+     OuterParse.opt_target --
+     OuterParse.fixes -- 
+     OuterParse.for_fixes --
+     Scan.optional 
+       (OuterParse.$$$ "where" |--
+          OuterParse.!!! 
+            (OuterParse.enum1 "|" 
+               (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}
 
 text {*
-  Note that the parser does not parse the ketword \simpleinductive. This 
-  will be done by the infrastructure that will eventually call this parser.
+  Note that the parser does not parse the keyword \simpleinductive, even if it is
+  meant to process definitions as shown above. The parser of the keyword 
+  will be given by the infrastructure that will eventually calls @{ML spec_parser}.
+  
+
   To see what the parser returns, let us parse the string corresponding to the 
   definition of @{term even} and @{term odd}:
 
@@ -638,9 +641,10 @@
       ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"}
 
   As can be seen, the result is a ``nested'' four-tuple consisting of an 
-  optional locale; a list of variables with optional type-annotation and  
-  syntax-annotation; a list of for-fixes (fixed variables); and a list of rules 
-  where each rule has optionally a name and an attribute.
+  optional locale (in this case @{ML NONE}); a list of variables with optional 
+  type-annotation and syntax-annotation; a list of for-fixes (fixed variables; in this
+  case there are none); and a list of rules where every rule has optionally a name and 
+  an attribute.
 
   In Line 2 of the parser, the function @{ML OuterParse.opt_target} reads a target 
   in order to indicate a locale in which the specification is made. For example
@@ -648,8 +652,8 @@
 @{ML_response [display,gray]
 "parse OuterParse.opt_target (filtered_input \"(in test)\")" "(SOME \"test\",[])"}
   
-  returns the locale @{text [quotes] "test"}; if no target is given' like in  the
-  casde of @{text "even"} and @{text "odd"}, the function returns @{ML NONE}.
+  returns the locale @{text [quotes] "test"}; if no target is given, like in  the
+  case of @{text "even"} and @{text "odd"}, the function returns @{ML NONE}.
 
   The function @{ML OuterParse.fixes} in Line 3 reads an \isacommand{and}-separated 
   list of variables that can include optional type annotations and syntax translations. 
@@ -671,7 +675,7 @@
 
 text {*
   Whenever types are given, they are stored in the @{ML SOME}s. Since types
-  are part of the inner syntax they are strings with some printing directives 
+  are part of the inner syntax they are strings with some encoded information 
   (see previous section). 
   If a syntax translation is present for a variable, then it is
   stored in the @{ML Mixfix} datastructure; no syntax translation is
@@ -701,7 +705,6 @@
   (name, map Args.dest_src attrib)
 end" "(foo_lemma, [((\"intro\", []), \<dots>), ((\"dest\", [\<dots>]), \<dots>)])"}
  
-  A name of a theorem can be quite complicated, as it can include attrinutes.
   The function @{ML opt_thm_name in SpecParse} is the ``optional'' variant of
   @{ML thm_name in SpecParse}. As can be seen each theorem name can contain some 
   attributes. If you want to print out all currently known attributes a theorem 
@@ -714,7 +717,7 @@
 \<dots>"}
 
 
-  For the inductive definitions described above only, the attibutes @{text "[intro]"} and
+  For the inductive definitions described above only the attibutes @{text "[intro]"} and
   @{text "[simp]"} make sense.
 
   \begin{readmore}

--- a/CookBook/Tactical.thy	Thu Feb 19 01:09:16 2009 +0000
+++ b/CookBook/Tactical.thy	Thu Feb 19 14:44:53 2009 +0000
@@ -398,8 +398,6 @@
 (*<*)oops(*>*)
 
 text {*
-  (FIXME: is it important to get the number of subgoals?)
- 
   The function @{ML resolve_tac} is similar to @{ML rtac}, except that it
   expects a list of theorems as arguments. From this list it will apply the
   first applicable theorem (later theorems that are also applicable can be

Binary file cookbook.pdf has changed