--- a/ProgTutorial/Tactical.thy	Fri Jul 31 19:10:39 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Sat Aug 01 08:59:41 2009 +0200
@@ -384,7 +384,7 @@
   Similarly, @{ML [index] rtac}, @{ML [index] dtac}, @{ML [index] etac} and 
   @{ML [index] ftac} correspond (roughly)
   to @{text rule}, @{text drule}, @{text erule} and @{text frule}, 
-  respectively. Each of them take a theorem as argument and attempt to 
+  respectively. Each of them takes a theorem as argument and attempts to 
   apply it to a goal. Below are three self-explanatory examples.
 *}
 
@@ -457,7 +457,7 @@
   into the goal state. Consider for example the proof
 *}
 
-lemma shows "\<forall>x\<in>A. P x \<Longrightarrow> Q x"
+lemma shows "\<forall>x \<in> A. P x \<Longrightarrow> Q x"
 apply(tactic {* dtac @{thm bspec} 1 *})
 txt{*\begin{minipage}{\textwidth}
      @{subgoals [display]} 
@@ -525,8 +525,9 @@
   Often proofs on the ML-level involve elaborate operations on assumptions and 
   @{text "\<And>"}-quantified variables. To do such operations using the basic tactics 
   shown so far is very unwieldy and brittle. Some convenience and
-  safety is provided by @{ML [index] SUBPROOF}. This tactic fixes the parameters 
-  and binds the various components of a goal state to a record. 
+  safety is provided by the functions @{ML [index] FOCUS} and @{ML [index] SUBPROOF}. 
+  These tactics fix the parameters 
+  and bind the various components of a goal state to a record. 
   To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which
   takes a record and just prints out the content of this record (using the 
   string transformation functions from in Section~\ref{sec:printing}). Consider
@@ -540,35 +541,33 @@
 *}
 
 
-ML{*fun sp_tac {prems, params, asms, concl, context, schematics} = 
+ML{*fun foc_tac {prems, params, asms, concl, context, schematics} = 
 let 
   val string_of_params = string_of_cterms context (map snd params)
-  val test = commas (map fst params)
   val string_of_asms = string_of_cterms context asms
   val string_of_concl = string_of_cterm context concl
   val string_of_prems = string_of_thms_no_vars context prems   
   val string_of_schms = string_of_cterms context (snd schematics)    
  
   val _ = (writeln ("params: " ^ string_of_params);
-           writeln ("param names: " ^ test);
            writeln ("schematics: " ^ string_of_schms);
            writeln ("assumptions: " ^ string_of_asms);
            writeln ("conclusion: " ^ string_of_concl);
            writeln ("premises: " ^ string_of_prems))
 in
-  no_tac 
+  all_tac 
 end*}
 text_raw{*
 \end{isabelle}
 \end{minipage}
-\caption{A function that prints out the various parameters provided by the tactic
- @{ML SUBPROOF}. It uses the functions defined in Section~\ref{sec:printing} for
+\caption{A function that prints out the various parameters provided by 
+ @{ML FOCUS} and @{ML SUBPROOF}. It uses the functions defined in Section~\ref{sec:printing} for
   extracting strings from @{ML_type cterm}s and @{ML_type thm}s.\label{fig:sptac}}
 \end{figure}
 *}
 
 lemma shows "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x"
-apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?
+apply(tactic {* FOCUS foc_tac @{context} 1 *})
 
 txt {*
   The tactic produces the following printout:
@@ -590,19 +589,11 @@
   @{prop "A x y"} is bound as @{ML_type cterm} to the record-variable 
   @{text asms}, but also as @{ML_type thm} to @{text prems}.
 
-  Notice also that we had to append @{text [quotes] "?"} to the
-  \isacommand{apply}-command. The reason is that @{ML [index] SUBPROOF} normally
-  expects that the subgoal is solved completely.  Since in the function @{ML
-  sp_tac} we returned the tactic @{ML no_tac}, the subproof obviously
-  fails. The question-mark allows us to recover from this failure in a
-  graceful manner so that the output messages are not overwritten by an 
-  ``empty sequence'' error message.
-
   If we continue the proof script by applying the @{text impI}-rule
 *}
 
 apply(rule impI)
-apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?
+apply(tactic {* FOCUS foc_tac @{context} 1 *})
 
 txt {*
   then the tactic prints out: 
@@ -622,10 +613,12 @@
 text {*
   Now also @{term "B y x"} is an assumption bound to @{text asms} and @{text prems}.
 
-  One convenience of @{ML SUBPROOF} is that we can apply the assumptions
-  using the usual tactics, because the parameter @{text prems} 
-  contains them as theorems. With this you can easily 
-  implement a tactic that behaves almost like @{ML atac}:
+  The difference between @{ML SUBPROOF} and @{ML FOCUS} is that the former
+  expects that the goal is solved completely, which the latter does not.  One
+  convenience of both @{ML FOCUS} and @{ML SUBPROOF} is that we can apply the
+  assumptions using the usual tactics, because the parameter @{text prems}
+  contains them as theorems. With this you can easily implement a tactic that
+  behaves almost like @{ML atac}:
 *}
 
 ML{*val atac' = SUBPROOF (fn {prems, ...} => resolve_tac prems 1)*}
@@ -664,11 +657,12 @@
 
 text {*
   \begin{readmore}
-  The function @{ML SUBPROOF} is defined in @{ML_file "Pure/subgoal.ML"} and
-  also described in \isccite{sec:results}. 
+  The functions @{ML FOCUS} and @{ML SUBPROOF} are defined in 
+  @{ML_file "Pure/subgoal.ML"} and also described in 
+  \isccite{sec:results}. 
   \end{readmore}
 
-  Similar but less powerful functions than @{ML SUBPROOF} are @{ML [index] SUBGOAL}
+  Similar but less powerful functions than @{ML FOCUS} are @{ML [index] SUBGOAL}
   and @{ML [index] CSUBGOAL}. They allow you to inspect a given subgoal (the former
   presents the subgoal as a @{ML_type term}, while the latter as a @{ML_type
   cterm}). With this you can implement a tactic that applies a rule according
@@ -699,7 +693,7 @@
   quantified variable. So you really have to construct the pattern using the
   basic term-constructors. This is not necessary in other cases, because their
   type is always fixed to function types involving only the type @{typ
-  bool}. (See Section \ref{sec:terms_manually} about constructing terms
+  bool}. (See Section \ref{sec:terms_types_manually} about constructing terms
   manually.) For the catch-all pattern, we chose to just return @{ML all_tac}. 
   Consequently, @{ML select_tac} never fails.
 
@@ -876,7 +870,7 @@
 *}
 
 ML{*val select_tac'' = TRY o FIRST' [rtac @{thm conjI}, rtac @{thm impI}, 
-                          rtac @{thm notI}, rtac @{thm allI}]*}
+                                 rtac @{thm notI}, rtac @{thm allI}]*}
 text_raw{*\label{tac:selectprimeprime}*}
 
 text {*