--- a/ProgTutorial/Tactical.thy	Thu Dec 03 14:19:13 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Fri Dec 04 23:45:32 2009 +0100
@@ -623,10 +623,13 @@
   latter does not. Another is that @{ML SUBPROOF} cannot instantiate any schematic
   variables.
 
-  One convenience of both @{ML FOCUS in Subgoal} 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}:
+  Observe that inside @{ML FOCUS in Subgoal} and @{ML SUBPROOF}, we are in a goal
+  state where there is only a conclusion. This means the tactics @{ML dtac} and 
+  the like are of no use for manipulating the goal state. The assumptions inside 
+  @{ML FOCUS in Subgoal} and @{ML SUBPROOF} are given as cterms and theorems in 
+  the arguments @{text "asms"} and @{text "prems"}, respectively. This 
+  means we can apply them using the usual assumption tactics. With this you can 
+  for example easily implement a tactic that behaves almost like @{ML atac}:
 *}
 
 ML{*val atac' = Subgoal.FOCUS (fn {prems, ...} => resolve_tac prems 1)*}
@@ -662,21 +665,55 @@
 
 
 text {*
+  There is one peculiarity about @{ML FOCUS in Subgoal} and @{ML SUBPROOF}.
+  If we apply @{text "rtac @{thm allI}"} in the proof below
+*}
+
+lemma
+  shows "B \<Longrightarrow> \<forall>x. A x"
+apply(tactic {* rtac @{thm allI} 1 *})
+txt{* it will produce the expected goal state
+      @{subgoals [display]} *}
+(*<*)oops(*>*)
+
+text {* But if we apply the same tactic inside @{ML FOCUS in Subgoal}
+  we obtain
+*}
+
+lemma
+  shows "B \<Longrightarrow> \<forall>x. A x"
+apply(tactic {* Subgoal.FOCUS (fn _ => rtac @{thm allI} 1) @{context} 1 *})
+txt{* it will produce the goal state
+      @{subgoals [display]} 
+
+  If we want to imitate the behaviour of the ``plain'' tactic, then we
+  can apply the tactic @{ML norm_hhf_tac in Goal}. This gives
+*}
+apply(tactic {* Goal.norm_hhf_tac 1 *})
+txt{*@{subgoals [display]}*}
+(*<*)oops(*>*)
+
+text {*
+  This tactic transforms the goal state into a \emph{hereditary Harrop normal
+  form}. To sum up, both @{ML FOCUS in Subgoal} and @{ML SUBPROOF} are rather
+  convenient, but can impose a considerable run-time penalty in automatic
+  proofs. If speed is of the essence, then maybe the two lower level combinators 
+  described next are more appropriate.
+
+
   \begin{readmore}
   The functions @{ML FOCUS in Subgoal} 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 FOCUS in Subgoal}, respectively
-  @{ML SUBPROOF}, are 
-  @{ML_ind SUBGOAL in Tactical} and @{ML_ind CSUBGOAL in Tactical}. They allow you to 
-  inspect a given subgoal (the former
+  Similar but less powerful functions than @{ML FOCUS in Subgoal},
+  respectively @{ML SUBPROOF}, are @{ML_ind SUBGOAL in Tactical} and @{ML_ind
+  CSUBGOAL in Tactical}. 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 them you can implement a tactic that applies a rule according
   to the topmost logic connective in the subgoal (to illustrate this we only
-  analyse a few connectives). The code of the tactic is as
-  follows.
+  analyse a few connectives). The code of the tactic is as follows.
 *}
 
 ML %linenosgray{*fun select_tac (t, i) =

Binary file progtutorial.pdf has changed