--- a/CookBook/FirstSteps.thy	Mon Feb 09 04:18:14 2009 +0000
+++ b/CookBook/FirstSteps.thy	Wed Feb 11 17:40:24 2009 +0000
@@ -171,11 +171,11 @@
 end" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
 
   The code about simpsets extracts the theorem names stored in the
-  current simpset.  We get hold of the current simpset with the antiquotation 
+  current simpset.  You can get hold of the current simpset with the antiquotation 
   @{text "@{simpset}"}.  The function @{ML rep_ss in MetaSimplifier} returns a record
   containing all information about the simpset. The rules of a simpset are
   stored in a \emph{discrimination net} (a data structure for fast
-  indexing). From this net we can extract the entries using the function @{ML
+  indexing). From this net you can extract the entries using the function @{ML
   Net.entries}.
 
 
@@ -258,7 +258,7 @@
   @{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 an coercion is inserted in the second component and 
+  where a coercion is inserted in the second component and 
 
   @{ML_response [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})" 
   "(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"}
@@ -345,7 +345,7 @@
 
   (FIXME: Is it useful to explain @{text "@{const_syntax}"}?)
 
-  Although to some extend types of terms can be inferred, there are many
+  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 
   type is as follows:
@@ -387,7 +387,7 @@
 
   A handy function for manipulating terms is @{ML map_types}: it takes a 
   function and applies it to every type in the term. You can, for example,
-  change every @{typ nat} into an @{typ int} using the function
+  change every @{typ nat} in a term into an @{typ int} using the function
 *}
 
 ML{*fun nat_to_int t =
@@ -411,7 +411,7 @@
 
 text {* 
   
-  You can freely construct and manipulate terms, since they are just
+  You can freely construct and manipulate @{ML_type "term"}s, since they are just
   arbitrary unchecked trees. However, you eventually want to see if a
   term is well-formed, or type-checks, relative to a theory.
   Type-checking is done via the function @{ML cterm_of}, which converts 
@@ -525,6 +525,8 @@
 
 section {* Storing Theorems *}
 
+text {* @{ML PureThy.add_thms_dynamic} *}
+
 section {* Theorem Attributes *}
 
 section {* Printing Terms and Theorems\label{sec:printing} *}
@@ -695,11 +697,11 @@
 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 one to read the code top-down.
+  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
-  one to get hold of an intermediate result (to do some side-calculations for
+  you to get hold of an intermediate result (to do some side-calculations for
   instance). The function
 
  *}
@@ -709,12 +711,13 @@
        |> tap (fn x => tracing (makestring x))
        |> (fn x => x + 2)*}
 
-text {* increments the argument first by one and then by two. 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.
+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
@@ -752,7 +755,7 @@
 ML{*fun (x, y) |-> f = f x y*}
 
 text {* and can be used to write the following roundabout version 
-  of the @{text double} function 
+  of the @{text double} function: 
 *}
 
 ML{*fun double x =
@@ -764,7 +767,7 @@
   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
+  for example, the function @{text double} can also be written as:
 *}
 
 ML{*val double =

--- a/CookBook/Intro.thy	Mon Feb 09 04:18:14 2009 +0000
+++ b/CookBook/Intro.thy	Wed Feb 11 17:40:24 2009 +0000
@@ -89,7 +89,7 @@
   
   Whenever appropriate we also show the response the code 
   generates when evaluated. This response is prefixed with a 
-  @{text [quotes] ">"} like:
+  @{text [quotes] ">"}, like:
 
   @{ML_response [display,gray] "3 + 4" "7"}
 

--- a/CookBook/Parsing.thy	Mon Feb 09 04:18:14 2009 +0000
+++ b/CookBook/Parsing.thy	Wed Feb 11 17:40:24 2009 +0000
@@ -37,7 +37,7 @@
 text {*
 
   Let us first have a look at parsing strings using generic parsing combinators. 
-  The function @{ML "(op $$)"} takes a string as argument and will ``consume'' this string from 
+  The function @{ML "$$"} takes a string as argument and will ``consume'' this string from 
   a given input list of strings. ``Consume'' in this context means that it will 
   return a pair consisting of this string and the rest of the input list. 
   For example:
@@ -61,13 +61,13 @@
   \item @{text "MORE"} indicates that there is not enough input for the parser. For example 
   in @{text "($$ \"h\") []"}.
   \item @{text "ABORT"} is the exception that is raised when a dead end is reached. 
-  It is used for example in the function @{ML "(op !!)"} (see below).
+  It is used for example in the function @{ML "!!"} (see below).
   \end{itemize}
 
   However, note that these exceptions are private to the parser and cannot be accessed
   by the programmer (for example to handle them).
   
-  Slightly more general than the parser @{ML "(op $$)"} is the function @{ML
+  Slightly more general than the parser @{ML "$$"} is the function @{ML
   Scan.one}, in that it takes a predicate as argument and then parses exactly
   one item from the input list satisfying this predicate. For example the
   following parser either consumes an @{text [quotes] "h"} or a @{text
@@ -84,7 +84,7 @@
 end"
     "((\"h\", [\"e\", \"l\", \"l\", \"o\"]),(\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
 
-  Two parser can be connected in sequence by using the function @{ML "(op --)"}. 
+  Two parser can be connected in sequence by using the function @{ML "--"}. 
   For example parsing @{text "h"}, @{text "e"} and @{text "l"} in this 
   sequence you can achieve by:
 
@@ -100,7 +100,7 @@
                           "(\"hell\", [\"o\"])"}
 
   Parsers that explore alternatives can be constructed using the function @{ML
-  "(op ||)"}. For example, the parser @{ML "(p || q)" for p q} returns the
+  "||"}. For example, the parser @{ML "(p || q)" for p q} returns the
   result of @{text "p"}, in case it succeeds, otherwise it returns the
   result of @{text "q"}. For example:
 
@@ -115,7 +115,7 @@
 end"
   "((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
 
-  The functions @{ML "(op |--)"} and @{ML "(op --|)"} work like the sequencing function 
+  The functions @{ML "|--"} and @{ML "--|"} work like the sequencing function 
   for parsers, except that they discard the item being parsed by the first (respectively second)
   parser. For example:
   
@@ -155,7 +155,7 @@
   (p input1, p input2)
 end" "((SOME \"h\", [\"e\", \"l\", \"l\", \"o\"]), (NONE, [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}
 
-  The function @{ML "(op !!)"} helps to produce appropriate error messages
+  The function @{ML "!!"} helps to produce appropriate error messages
   during parsing. For example if you want to parse that @{text p} is immediately 
   followed by @{text q}, or start a completely different parser @{text r},
   you might write:
@@ -171,7 +171,7 @@
   circumstance this will be the wrong parser for the input ``p-followed-by-q''
   and therefore will also fail. The error message is then caused by the
   failure of @{text r}, not by the absence of @{text q} in the input. This
-  kind of situation can be avoided when using the function @{ML "(op !!)"}. 
+  kind of situation can be avoided when using the function @{ML "!!"}. 
   This function aborts the whole process of parsing in case of a
   failure and prints an error message. For example if you invoke the parser
 
@@ -189,7 +189,7 @@
   @{ML_response_fake [display,gray] "(!! (fn _ => \"foo\") ($$ \"h\")) (explode \"world\")"
                                "Exception ABORT raised"}
 
-  then the parsing aborts and the error message @{text "foo"} is printed out. In order to
+  then the parsing aborts and the error message @{text "foo"} is printed. In order to
   see the error message properly, we need to prefix the parser with the function 
   @{ML "Scan.error"}. For example:
 
@@ -430,7 +430,7 @@
 end"
 "((\"where\",\<dots>),(\"|\",\<dots>))"}
 
-  Like before, you can sequentially connect parsers with @{ML "(op --)"}. For example: 
+  Like before, you can sequentially connect parsers with @{ML "--"}. For example: 
 
 @{ML_response [display,gray]
 "let 
@@ -571,7 +571,7 @@
   (FIXME: should for-fixes take any syntax annotation?)
 
   @{ML OuterParse.for_fixes} is an ``optional'' that prefixes 
-  @{ML OuterParse.fixes} with the comman \isacommand{for}.
+  @{ML OuterParse.fixes} with the command \isacommand{for}.
   (FIXME give an example and explain more)
 
 @{ML_response [display,gray]

--- a/CookBook/Tactical.thy	Mon Feb 09 04:18:14 2009 +0000
+++ b/CookBook/Tactical.thy	Wed Feb 11 17:40:24 2009 +0000
@@ -21,7 +21,7 @@
 
 text {*
   To see how tactics work, let us first transcribe a simple \isacommand{apply}-style proof 
-  into ML. Consider the following proof.
+  into ML. Suppose the following proof.
 *}
 
 lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"
@@ -62,18 +62,17 @@
 
   \begin{readmore}
   To learn more about the function @{ML Goal.prove} see \isccite{sec:results}
-  and the file @{ML_file "Pure/goal.ML"}. For more information about the
-  internals of goals see \isccite{sec:tactical-goals}.  See @{ML_file
+  and the file @{ML_file "Pure/goal.ML"}.  See @{ML_file
   "Pure/tactic.ML"} and @{ML_file "Pure/tctical.ML"} for the code of basic
   tactics and tactic combinators; see also Chapters 3 and 4 in the old
   Isabelle Reference Manual.
   \end{readmore}
 
-  Note that we used antiquotations for referencing the theorems. Many theorems
+  Note that in the code above we used antiquotations for referencing the theorems. Many theorems
   also have ML-bindings with the same name. Therefore, we could also just have
   written @{ML "etac disjE 1"}, or in case there are no ML-binding obtained
   the theorem dynamically using the function @{ML thm}; for example 
-  @{ML "etac (thm \"disjE\") 1"}. Both ways however are considered bad style. 
+  @{ML "etac (thm \"disjE\") 1"}. Both ways however are considered bad style! 
   The reason
   is that the binding for @{ML disjE} can be re-assigned by the user and thus
   one does not have complete control over which theorem is actually
@@ -133,7 +132,7 @@
 
 text {*
   This kind of addressing is more difficult to achieve when the goal is 
-  hard-coded inside the tactic. For every operator that combines tactics 
+  hard-coded inside the tactic. For most operators that combine tactics 
   (@{ML THEN} is only one such operator) a ``primed'' version exists.
 
   The tactics @{ML foo_tac} and @{ML foo_tac'} are very specific for
@@ -175,7 +174,7 @@
 
   The lazy list of possible successor states shows through at the user-level 
   of Isabelle when using the command \isacommand{back}. For instance in the 
-  following proof, there are two possibilities for how to apply 
+  following proof there are two possibilities for how to apply 
   @{ML foo_tac'}: either using the first assumption or the second.
 *}
 
@@ -215,7 +214,7 @@
 text {*
   which prints out the given theorem (using the string-function defined 
   in Section~\ref{sec:printing}) and then behaves like @{ML all_tac}. We
-  are now in the position to inspect every proof state in a proof. Consider 
+  are now in the position to inspect every goal state in a proof. Consider 
   the proof below: on the left-hand side we show the goal state as shown 
   by Isabelle, on the right-hand side the print out from @{ML my_print_tac}.
 *}
@@ -224,48 +223,48 @@
 apply(tactic {* my_print_tac @{context} *})
 
 txt{* \small 
-      \begin{tabular}{@ {}l@ {}p{0.7\textwidth}@ {}}
+      \begin{tabularstar}{\textwidth}{@ {}l@ {\extracolsep{\fill}}l@ {}}
       \begin{minipage}[t]{0.3\textwidth}
       @{subgoals [display]} 
       \end{minipage} &
-      \hfill@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
-      \end{tabular}
+      @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
+      \end{tabularstar}
 *}
 
 apply(rule conjI)
 apply(tactic {* my_print_tac @{context} *})
 
 txt{* \small 
-      \begin{tabular}{@ {}l@ {}p{0.76\textwidth}@ {}}
+      \begin{tabularstar}{\textwidth}{@ {}l@ {\extracolsep{\fill}}l@ {}}
       \begin{minipage}[t]{0.26\textwidth}
       @{subgoals [display]} 
       \end{minipage} &
-      \hfill@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
-      \end{tabular}
+      @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
+      \end{tabularstar}
 *}
 
 apply(assumption)
 apply(tactic {* my_print_tac @{context} *})
 
 txt{* \small 
-      \begin{tabular}{@ {}l@ {}p{0.7\textwidth}@ {}}
+      \begin{tabularstar}{\textwidth}{@ {}l@ {\extracolsep{\fill}}l@ {}}
       \begin{minipage}[t]{0.3\textwidth}
       @{subgoals [display]} 
       \end{minipage} &
-      \hfill@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
-      \end{tabular}
+      @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
+      \end{tabularstar}
 *}
 
 apply(assumption)
 apply(tactic {* my_print_tac @{context} *})
 
 txt{* \small 
-      \begin{tabular}{@ {}l@ {}p{0.7\textwidth}@ {}}
+      \begin{tabularstar}{\textwidth}{@ {}l@ {\extracolsep{\fill}}l@ {}}
       \begin{minipage}[t]{0.3\textwidth}
       @{subgoals [display]} 
       \end{minipage} &
-      \hfill@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}
-      \end{tabular}
+      @{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}
+      \end{tabularstar}
 *}
 
 done
@@ -277,7 +276,7 @@
 
   where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are the  
   subgoals. So after setting up the lemma, the goal state is always of the form
-  @{text "C \<Longrightarrow> (C)"}, and when the proof is finished we are left with @{text "(C)"}. 
+  @{text "C \<Longrightarrow> (C)"}; when the proof is finished we are left with @{text "(C)"}. 
   Since the goal @{term C} can potentially be an implication, 
   there is a ``protector'' wrapped around it (in from of an outermost constant 
   @{text "Const (\"prop\", bool \<Rightarrow> bool)"} applied to each goal;
@@ -285,8 +284,13 @@
   prevents that premises of @{text C} are mis-interpreted as open subgoals. 
   While tactics can operate on the subgoals (the @{text "A\<^isub>i"} above), they 
   are expected to leave the conclusion @{term C} intact, with the 
-  exception of possibly instantiating schematic variables. 
+  exception of possibly instantiating schematic variables. If you use
+  the predefined tactics, this will always be the case. 
  
+  \begin{readmore}
+  For more information about the internals of goals see \isccite{sec:tactical-goals}.
+  \end{readmore}
+
 *}
 
 section {* Simple Tactics *}
@@ -396,16 +400,33 @@
 
 text {*
   Since rules are applied using higher-order unification, an automatic proof
-  procedure might become too fragile, if it just applies inference rules shown
-  in the fashion above.  More constraints can be introduced by
-  pre-instantiating theorems with other theorems. You can do this using the
-  function @{ML RS}. For example
+  procedure might become too fragile, if it just applies inference rules as 
+  shown above. The reason is that a number of rules introduce meta-variables 
+  into the goal state. Consider for example the proof
+*}
+
+lemma shows "\<forall>x\<in>A. P x \<Longrightarrow> Q x"
+apply(drule bspec)
+txt{*\begin{minipage}{\textwidth}
+     @{subgoals [display]} 
+     \end{minipage}*}
+(*<*)oops(*>*)
+
+text {*
+  where the application of @{text bspec} results into two subgoals involving the
+  meta-variable @{text "?x"}. The point is that if you are not careful, tactics 
+  applied to the first subgoal might instantiate this meta-variable in such a 
+  way that the second subgoal becomes unprovable. If it is clear what the @{text "?x"}
+  should be, then this situation can be avoided by introducing a more
+  constraint version of the @{text bspec}-rule. Such constraints can be enforced by
+  pre-instantiating theorems with other theorems, for example by using the
+  function @{ML RS}
   
   @{ML_response_fake [display,gray]
   "@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}
 
-  instantiates the first premise of the @{text conjI}-rule with the
-  rule @{text disjI1}. If this is impossible, as in the case of
+  which, for instance, instantiates the first premise of the @{text conjI}-rule 
+  with the rule @{text disjI1}. If this is impossible, as in the case of
 
   @{ML_response_fake_both [display,gray]
   "@{thm conjI} RS @{thm mp}" 
@@ -613,7 +634,7 @@
    | _ => all_tac*}
 
 text {*
-  In line 3 you need to decend under the outermost @{term "Trueprop"} in order
+  In line 3 you need to descend under the outermost @{term "Trueprop"} in order
   to get to the connective you like to analyse. Otherwise goals like @{prop "A \<and> B"} 
   are not properly analysed. While for the first four pattern we can use the 
   @{text "@term"}-antiquotation, the pattern in Line 7 cannot be constructed
@@ -621,7 +642,7 @@
   quantified variable. So you really have to construct the pattern
   using the term-constructors. This is not necessary in  other cases, because 
   their type is always something involving @{typ bool}. The final patter is 
-  for the case where the goal does not fall into any of the categorories before.
+  for the case where the goal does not fall into any of the categories before.
   In this case we chose to just return @{ML all_tac} (i.e., @{ML select_tac} 
   never fails). 
 
@@ -643,7 +664,7 @@
   where in all but the last the tactic applied an introduction rule. 
   Note that we applied the tactic to subgoals in ``reverse'' order. 
   This is a trick in order to be independent from what subgoals are 
-  that are produced by the rule. If we had it applied in the other order 
+  that are produced by the rule. If we had applied it in the other order 
 *}
 
 lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
@@ -659,7 +680,7 @@
   the ``reverse application'' is easy to implement.
 
   However, this example is very contrived: there are much simpler methods to implement
-  such a proof procedure analying a goal according to its topmost
+  such a proof procedure analysing a goal according to its topmost
   connective. These simpler methods use tactic combinators which will be explained 
   in the next section.
 *}
@@ -668,7 +689,7 @@
 
 text {* 
   The purpose of tactic combinators is to build powerful tactics out of
-  smaller components. In the previous section we already used @{ML THEN} which
+  smaller components. In the previous section we already used @{ML THEN}, which
   strings two tactics together in sequence. For example:
 *}
 
@@ -681,7 +702,7 @@
 
 text {*
   If you want to avoid the hard-coded subgoal addressing, then you can use
-  the ``primed'' version of @{ML THEN}, namely @{ML THEN'}. For example:
+  the ``primed'' version of @{ML THEN}. For example:
 *}
 
 lemma shows "(Foo \<and> Bar) \<and> False"
@@ -698,28 +719,27 @@
   If there is a list of tactics that should all be tried out in 
   sequence, you can use the combinator @{ML EVERY'}. For example
   the function @{ML foo_tac'} from page~\ref{tac:footacprime} can also 
-  be written as
+  be written as:
 *}
 
 ML{*val foo_tac'' = EVERY' [etac @{thm disjE}, rtac @{thm disjI2}, 
                         atac, rtac @{thm disjI1}, atac]*}
 
 text {*
-  There is even another variant for @{ML foo_tac''}: in automatic proof
-  procedures (in contrast to tactics that might be called by the user) 
-  there are often long lists of tactics that are applied to the first
-  subgoal. Instead of writing the code above and then calling 
-  @{ML "foo_tac'' 1"}, you can also just write
+  There is even another way: in automatic proof procedures (in contrast to
+  tactics that might be called by the user) there are often long lists of
+  tactics that are applied to the first subgoal. Instead of writing the code
+  above and then calling @{ML "foo_tac'' 1"}, you can also just write
 *}
 
 ML{*val foo_tac1 = EVERY1 [etac @{thm disjE}, rtac @{thm disjI2}, 
-                         atac, rtac @{thm disjI1}, atac]*}
+                       atac, rtac @{thm disjI1}, atac]*}
 
 text {*
   With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML EVERY1} it must be 
-  guaranteed that  all component tactics sucessfully apply; otherwise the 
+  guaranteed that  all component tactics successfully apply; otherwise the 
   whole tactic will fail. If you rather want to try out a number of tactics, 
-  then you can use the combinator @{ML ORELSE'} for two tactics and @{ML FIRST'} 
+  then you can use the combinator @{ML ORELSE'} for two tactics, and @{ML FIRST'} 
   (or @{ML FIRST1}) for a list of tactics. For example, the tactic
 *}
 
@@ -731,8 +751,8 @@
 *}
 
 lemma shows "True \<and> False" and "Foo \<or> Bar"
+apply(tactic {* orelse_xmp 2 *})
 apply(tactic {* orelse_xmp 1 *})
-apply(tactic {* orelse_xmp 3 *})
 txt {* which results in the goal state
 
        \begin{minipage}{\textwidth}
@@ -751,10 +771,10 @@
                           rtac @{thm notI}, rtac @{thm allI}, K all_tac]*}
 
 text {*
-  Since we like to mimic the bahaviour of @{ML select_tac}, we must include
-  @{ML all_tac} at the end (@{ML all_tac} must also be ``wrapped up'' using
-  the @{ML K}-combinator as it does not take a subgoal number as argument). 
-  We can test the tactic on the same proof:
+  Since we like to mimic the behaviour of @{ML select_tac} as closely as possible, 
+  we must include @{ML all_tac} at the end of the list (@{ML all_tac} must also 
+  be ``wrapped up'' using the @{ML K}-combinator, as it does not take a subgoal 
+  number as argument). We can test the tactic on the same proof:
 *}
 
 lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
@@ -768,10 +788,10 @@
 (*<*)oops(*>*)
 
 text {* 
-  and obtain the same subgoals. Since this repeated application of a tactic
-  to the reverse order of \emph{all} subgoals is quite common, there is 
-  the tactics combinator @{ML ALLGOALS} that simplifies this. Using this 
-  combinator we can simply write: *}
+  Because such repeated applications of a tactic to the reverse order of 
+  \emph{all} subgoals is quite common, there is the tactics combinator 
+  @{ML ALLGOALS} that simplifies this. Using this combinator we can simply 
+  write: *}
 
 lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
 apply(tactic {* ALLGOALS select_tac' *})
@@ -781,9 +801,9 @@
 (*<*)oops(*>*)
 
 text {*
-  We chose to write @{ML select_tac'} in such a way that it always succeeds.
-  This can be potetially very  confusing for the user in cases of goals 
-  of the form
+  Remember that we chose to write @{ML select_tac'} in such a way that it always 
+  succeeds. This can be potentially very confusing for the user, for example,  
+  in cases the goals is the form
 *}
 
 lemma shows "E \<Longrightarrow> F"
@@ -796,24 +816,131 @@
 text {*
   where no rule applies. The reason is that the user has little chance 
   to see whether progress in the proof has been made or not. We could simply
-  remove @{ML "K all_tac"} from the end of the list. Then the tactic would
-  only apply in cases where it can make some progress. But for the sake of
-  argument, let us assume that this is not an option. In such cases, you 
+  delete th @{ML "K all_tac"} from the end of the list. Then @{ML select_tac'} 
+  would only succeed on goals where it can make progress. But for the sake of
+  argument, let us suppose that this deletion is not an option. In such cases, you 
   can use the combinator @{ML CHANGED} to make sure the subgoal has been
   changed by the tactic. Because now
 *}
 
 lemma shows "E \<Longrightarrow> F"
 apply(tactic {* CHANGED (select_tac' 1) *})(*<*)?(*>*)
-txt{* results in the usual error message for empty result sequences. *}
-(*<*)oops(*>*)
+txt{* results in the error message:
+  \begin{isabelle}
+  @{text "*** empty result sequence -- proof command failed"}\\
+  @{text "*** At command \"apply\"."}
+  \end{isabelle} 
+*}(*<*)oops(*>*)
 
 
 text {*
+  Meaning the tactic failed. 
 
-  @{ML REPEAT} @{ML DETERM}
+  We can extend @{ML select_tac'} so that it not just applies to the top-most
+  connective, but also to the ones immediately ``underneath''. For this you can use the
+  tactic combinator @{ML REPEAT}. For example suppose the following tactic
+*}
+
+ML{*val repeat_xmp = REPEAT (CHANGED (select_tac' 1)) *}
+
+text {* and the proof *}
+
+lemma shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"
+apply(tactic {* repeat_xmp *})
+txt{* \begin{minipage}{\textwidth}
+      @{subgoals [display]}
+      \end{minipage} *}
+(*<*)oops(*>*)
+
+text {*
+  Here it is crucial that @{ML select_tac'} is prefixed with @{ML CHANGED}, 
+  because otherwise @{ML REPEAT} runs into an infinite loop. The function
+  @{ML REPEAT1} is similar, but runs the tactic at least once (failing if 
+  this is not possible).
+
+  If you are after the ``primed'' version of @{ML repeat_xmp} then it 
+  needs to be coded as
+*}
+
+ML{*val repeat_xmp' = REPEAT o CHANGED o select_tac'*}
+
+text {*
+  since there are no ``primed'' versions of @{ML REPEAT} and @{ML CHANGED}.
+
+  If you look closely at the goal state above, the tactics @{ML repeat_xmp}
+  and @{ML repeat_xmp'} are not yet quite what we are after: the problem is
+  that goals 2 and 3 are not yet analysed. This is because both tactics
+  apply repeatedly only to the first subgoal. To analyse also all
+  resulting subgoals, you can use the function @{ML REPEAT_ALL_NEW}. 
+  Suppose the tactic
+*}
+
+ML{*val repeat_all_new_xmp = REPEAT_ALL_NEW (CHANGED o select_tac')*}
+
+text {* 
+  which analyses the topmost connectives also in all resulting 
+  subgoals.
+*}
+
+lemma shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"
+apply(tactic {* repeat_all_new_xmp 1 *})
+txt{* \begin{minipage}{\textwidth}
+      @{subgoals [display]}
+      \end{minipage} *}
+(*<*)oops(*>*)
 
-  @{ML CHANGED}
+text {*
+  The last tactic combinator we describe here is @{ML DETERM}. Recall 
+  that tactics produce a lazy sequence of successor goal states. These
+  states can be explored using the command \isacommand{back}. For example
+
+*}
+
+lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
+apply(tactic {* etac @{thm disjE} 1 *})
+txt{* applies the rule to the first assumption
+      
+      \begin{minipage}{\textwidth}
+      @{subgoals [display]}
+      \end{minipage} *}
+(*<*)
+oops
+lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
+apply(tactic {* etac @{thm disjE} 1 *})
+(*>*)
+back
+txt{* whereas it is now applied to the second
+
+      \begin{minipage}{\textwidth}
+      @{subgoals [display]}
+      \end{minipage} *}
+(*<*)oops(*>*)
+
+text {*
+  Sometimes this leads to confusing behaviour of tactics and also has
+  the potential to explode the search space for tactics build on top.
+  This can be avoided by prefixing the tactic with @{ML DETERM}.
+*}
+
+lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
+apply(tactic {* DETERM (etac @{thm disjE} 1) *})
+txt {*\begin{minipage}{\textwidth}
+      @{subgoals [display]}
+      \end{minipage} *}
+(*<*)oops(*>*)
+text {*
+  This will prune the search space to just the first possibility.
+  Attempting to apply \isacommand{back} in this goal states gives the
+  error message:
+
+  \begin{isabelle}
+  @{text "*** back: no alternatives"}\\
+  @{text "*** At command \"back\"."}
+  \end{isabelle}
+
+  \begin{readmore}
+  Most tactic combinators are defined in @{ML_file "Pure/tctical.ML"}.
+  \end{readmore}
 
 *}
 

--- a/CookBook/document/root.tex	Mon Feb 09 04:18:14 2009 +0000
+++ b/CookBook/document/root.tex	Wed Feb 11 17:40:24 2009 +0000
@@ -99,6 +99,11 @@
 \newcommand{\isasymverbclose}{\isacharverbatimclose}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% since * cannot be used in text {*...*} 
+\newenvironment{tabularstar}[2]
+{\begin{tabular*}{#1}{#2}}{\end{tabular*}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{document}
 
 \title{\mbox{}\\[-10ex]

Binary file cookbook.pdf has changed