diff -r f286dfa9f173 -r 2728e8daebc0 ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Mon Aug 03 13:53:04 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Mon Aug 03 14:01:57 2009 +0200
@@ -145,7 +145,7 @@
   @{text "*** At command \"apply\"."}
   \end{isabelle}
 
-  This means they failed.\footnote{To be precise tactics do not produce this error
+  This means they failed.\footnote{To be precise, tactics do not produce this error
   message, it originates from the \isacommand{apply} wrapper.} The reason for this 
   error message is that tactics 
   are functions mapping a goal state to a (lazy) sequence of successor states. 
@@ -212,7 +212,7 @@
 
 ML{*fun my_print_tac ctxt thm =
 let
-  val _ = writeln (string_of_thm_no_vars ctxt thm)
+  val _ = tracing (string_of_thm_no_vars ctxt thm)
 in 
   Seq.single thm
 end*}
@@ -528,9 +528,8 @@
   safety is provided by the functions @{ML [index] FOCUS in Subgoal} 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
+  To see what happens, use the function defined in Figure~\ref{fig:sptac}, which
+  takes a record and just prints out the contents of this record. Consider
   now the proof:
 *}
 
@@ -549,11 +548,11 @@
   val string_of_prems = string_of_thms_no_vars context prems   
   val string_of_schms = string_of_cterms context (map fst (snd schematics))    
  
-  val _ = (writeln ("params: " ^ string_of_params);
-           writeln ("schematics: " ^ string_of_schms);
-           writeln ("assumptions: " ^ string_of_asms);
-           writeln ("conclusion: " ^ string_of_concl);
-           writeln ("premises: " ^ string_of_prems))
+  val _ = (tracing ("params: " ^ string_of_params);
+           tracing ("schematics: " ^ string_of_schms);
+           tracing ("assumptions: " ^ string_of_asms);
+           tracing ("conclusion: " ^ string_of_concl);
+           tracing ("premises: " ^ string_of_prems))
 in
   all_tac 
 end*}
@@ -577,19 +576,19 @@
   \begin{quote}\small
   \begin{tabular}{ll}
   params:      & @{term x}, @{term y}\\
-  schematics:  & @{term z}\\
+  schematics:  & @{text ?z}\\
   assumptions: & @{term "A x y"}\\
   conclusion:  & @{term "B y x \<longrightarrow> C (z y) x"}\\
   premises:    & @{term "A x y"}
   \end{tabular}
   \end{quote}
 
-  (FIXME: find out how nowadays the schmetics are handled)
+  (FIXME: Find out how nowadays the schematics are handled)
 
-  Notice in the actual output the brown colour of the variables @{term x} and 
-  @{term y}. Although they are parameters in the original goal, they are fixed inside
-  the subproof. By convention these fixed variables are printed in brown colour.
-  Similarly the schematic variable @{term z}. The assumption, or premise, 
+  Notice in the actual output the brown colour of the variables @{term x}, 
+  and @{term y}. Although they are parameters in the original goal, they are fixed inside
+  the tactic. By convention these fixed variables are printed in brown colour.
+  Similarly the schematic variable @{text ?z}. The assumption, or premise, 
   @{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}.
 
@@ -605,7 +604,7 @@
   \begin{quote}\small
   \begin{tabular}{ll}
   params:      & @{term x}, @{term y}\\
-  schematics:  & @{term z}\\
+  schematics:  & @{text ?z}\\
   assumptions: & @{term "A x y"}, @{term "B y x"}\\
   conclusion:  & @{term "C (z y) x"}\\
   premises:    & @{term "A x y"}, @{term "B y x"}
@@ -617,15 +616,18 @@
 text {*
   Now also @{term "B y x"} is an assumption bound to @{text asms} and @{text prems}.
 
-  The difference between @{ML SUBPROOF} and @{ML FOCUS in Subgoal} is that the former
-  expects that the goal is solved completely, which the latter does not.  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}:
+  The difference between the tactics @{ML SUBPROOF} and @{ML FOCUS in Subgoal}
+  is that the former expects that the goal is solved completely, which the
+  latter does not. @{ML SUBPROOF} can also not instantiate an 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}:
 *}
 
-ML{*val atac' = SUBPROOF (fn {prems, ...} => resolve_tac prems 1)*}
+ML{*val atac' = Subgoal.FOCUS (fn {prems, ...} => resolve_tac prems 1)*}
 
 text {*
   If you apply @{ML atac'} to the next lemma
@@ -638,19 +640,14 @@
 (*<*)oops(*>*)
 
 text {*
-  The restriction in this tactic which is not present in @{ML atac} is that it
-  cannot instantiate any schematic variables. This might be seen as a defect,
-  but it is actually an advantage in the situations for which @{ML SUBPROOF}
-  was designed: the reason is that, as mentioned before, instantiation of
-  schematic variables can affect several goals and can render them
-  unprovable. @{ML SUBPROOF} is meant to avoid this.
+  Notice that @{ML atac'} inside @{ML FOCUS in Subgoal} calls @{ML
+  resolve_tac} with the subgoal number @{text "1"} and also the outer call to
+  @{ML FOCUS in Subgoal} in the \isacommand{apply}-step uses @{text "1"}. This
+  is another advantage of @{ML FOCUS in Subgoal} and @{ML SUBPROOF}: the
+  addressing inside it is completely local to the tactic inside the
+  subproof. It is therefore possible to also apply @{ML atac'} to the second
+  goal by just writing:
 
-  Notice that @{ML atac'} inside @{ML SUBPROOF} calls @{ML resolve_tac} with
-  the subgoal number @{text "1"} and also the outer call to @{ML SUBPROOF} in
-  the \isacommand{apply}-step uses @{text "1"}. This is another advantage of
-  @{ML SUBPROOF}: the addressing inside it is completely local to the tactic
-  inside the subproof. It is therefore possible to also apply @{ML atac'} to
-  the second goal by just writing:
 *}
 
 lemma shows "True" and "\<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
@@ -666,7 +663,8 @@
   \isccite{sec:results}. 
   \end{readmore}
 
-  Similar but less powerful functions than @{ML FOCUS in Subgoal} are 
+  Similar but less powerful functions than @{ML FOCUS in Subgoal}, respectively
+  @{ML SUBPROOF}, 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
@@ -1196,7 +1194,7 @@
           ["Simproc patterns:"] @ map name_ctrm procs
 in
   s |> cat_lines
-    |> writeln
+    |> tracing
 end*}
 text_raw {* 
 \end{isabelle}
@@ -1523,7 +1521,7 @@
 ML %linenosgray{*fun fail_simproc simpset redex = 
 let
   val ctxt = Simplifier.the_context simpset
-  val _ = writeln ("The redex: " ^ (string_of_cterm ctxt redex))
+  val _ = tracing ("The redex: " ^ (string_of_cterm ctxt redex))
 in
   NONE
 end*}
@@ -1594,7 +1592,7 @@
 ML{*fun fail_simproc' simpset redex = 
 let
   val ctxt = Simplifier.the_context simpset
-  val _ = writeln ("The redex: " ^ (Syntax.string_of_term ctxt redex))
+  val _ = tracing ("The redex: " ^ (Syntax.string_of_term ctxt redex))
 in
   NONE
 end*}