--- a/ProgTutorial/Base.thy	Mon Aug 03 13:53:04 2009 +0200
+++ b/ProgTutorial/Base.thy	Mon Aug 03 14:01:57 2009 +0200
@@ -7,6 +7,7 @@
 begin
 
 (* to have a special tag for text enclosed in ML *)
+
 ML {*
 
 fun propagate_env (context as Context.Proof lthy) =
@@ -37,5 +38,4 @@
 
 *}
 
-
 end
\ No newline at end of file

--- a/ProgTutorial/FirstSteps.thy	Mon Aug 03 13:53:04 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Mon Aug 03 14:01:57 2009 +0200
@@ -4,7 +4,6 @@
 
 chapter {* First Steps *}
 
-
 text {*
   Isabelle programming is done in ML. Just like lemmas and proofs, ML-code
   in Isabelle is part of a theory. If you want to follow the code given in
@@ -230,7 +229,7 @@
   @{text "?Q"} and so on. 
 
   @{ML_response_fake [display, gray]
-  "writeln (string_of_thm @{context} @{thm conjI})"
+  "tracing (string_of_thm @{context} @{thm conjI})"
   "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
 
   In order to improve the readability of theorems we convert
@@ -252,7 +251,7 @@
   Theorem @{thm [source] conjI} is now printed as follows:
 
   @{ML_response_fake [display, gray]
-  "writeln (string_of_thm_no_vars @{context} @{thm conjI})"
+  "tracing (string_of_thm_no_vars @{context} @{thm conjI})"
   "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"}
   
   Again the function @{ML commas} helps with printing more than one theorem. 
@@ -359,7 +358,7 @@
 in 
   apply_fresh_args t ctxt
    |> Syntax.string_of_term ctxt
-   |> writeln
+   |> tracing
 end" 
   "P z za zb"}
 
@@ -384,7 +383,7 @@
 in
   apply_fresh_args t ctxt 
    |> Syntax.string_of_term ctxt
-   |> writeln
+   |> tracing
 end"
   "za z zb"}
   
@@ -743,9 +742,9 @@
   val v2 = Var ((\"x1\", 3), @{typ bool})
   val v3 = Free (\"x\", @{typ bool})
 in
-  writeln (Syntax.string_of_term @{context} v1);
-  writeln (Syntax.string_of_term @{context} v2);
-  writeln (Syntax.string_of_term @{context} v3)
+  tracing (Syntax.string_of_term @{context} v1);
+  tracing (Syntax.string_of_term @{context} v2);
+  tracing (Syntax.string_of_term @{context} v3)
 end"
 "?x3
 ?x1.3
@@ -776,7 +775,7 @@
 "let
   val omega = Free (\"x\", @{typ nat}) $ Free (\"x\", @{typ nat})
 in 
-  writeln (Syntax.string_of_term @{context} omega)
+  tracing (Syntax.string_of_term @{context} omega)
 end"
   "x x"}
 
@@ -980,7 +979,7 @@
 "let
   val eq = HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})
 in
-  writeln (Syntax.string_of_term @{context} eq)
+  tracing (Syntax.string_of_term @{context} eq)
 end"
   "True = False"}
 *}
@@ -1908,7 +1907,7 @@
          case realOut (!r) of
             NONE => "NONE"
           | SOME x => Real.toString x
-      val () = writeln (concat [s1, " ", s2, " ", s3, "\n"])
+      val () = tracing (concat [s1, " ", s2, " ", s3, "\n"])
    end*}
 
 ML_val{*structure t = Test(U) *} 
@@ -1985,7 +1984,7 @@
   type:
 *}
 
-ML{*fun pprint prt = writeln (Pretty.string_of prt)*}
+ML{*fun pprint prt = tracing (Pretty.string_of prt)*}
 
 text {*
   The point of the pretty-printing infrastructure is to give hints about how to
@@ -2008,7 +2007,7 @@
   we obtain the ugly output:
 
 @{ML_response_fake [display,gray]
-"writeln test_str"
+"tracing test_str"
 "fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo
 ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa
 aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo
@@ -2212,12 +2211,12 @@
 text {* the infrastructure of Syntax-pretty-term makes sure it is printed nicely  *}
 
 
-ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of  |> writeln *}
-ML {* (Pretty.str "bar") |> Pretty.string_of |> writeln *}
-
-
-ML {* Pretty.mark Markup.subgoal (Pretty.str "foo") |> Pretty.string_of  |> writeln *}
-ML {* (Pretty.str "bar") |> Pretty.string_of |> writeln *}
+ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of  |> tracing *}
+ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *}
+
+
+ML {* Pretty.mark Markup.subgoal (Pretty.str "foo") |> Pretty.string_of  |> tracing *}
+ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *}
 
 text {*
   Still to be done:
@@ -2238,8 +2237,8 @@
 *}
 
 
-ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of  |> writeln *}
-ML {* (Pretty.str "bar") |> Pretty.string_of |> writeln *}
+ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of  |> tracing *}
+ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *}
 
 text {* writing into the goal buffer *}
 
@@ -2260,4 +2259,5 @@
 
 section {* Name Space(TBD) *}
 
+
 end

--- a/ProgTutorial/Package/Ind_Code.thy	Mon Aug 03 13:53:04 2009 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy	Mon Aug 03 14:01:57 2009 +0200
@@ -50,7 +50,7 @@
   val arg = ((@{binding "My_True"}, NoSyn), @{term True})
   val (def, lthy') = make_defn arg lthy 
 in
-  writeln (string_of_thm_no_vars lthy' def); lthy'
+  tracing (string_of_thm_no_vars lthy' def); lthy'
 end *}
 
 text {*
@@ -117,7 +117,7 @@
 let
   val def = defn_aux lthy eo_orules eo_preds (e_pred, e_arg_tys)
 in
-  writeln (Syntax.string_of_term lthy def); lthy
+  tracing (Syntax.string_of_term lthy def); lthy
 end *}
 
 text {*
@@ -137,7 +137,7 @@
   val def = defn_aux lthy fresh_orules 
                              [fresh_pred] (fresh_pred, fresh_arg_tys)
 in
-  writeln (Syntax.string_of_term lthy def); lthy
+  tracing (Syntax.string_of_term lthy def); lthy
 end *}
 
 
@@ -187,7 +187,7 @@
   val (defs, lthy') = 
     defns eo_rules eo_preds eo_prednames eo_mxs eo_arg_tyss lthy
 in
-  writeln (string_of_thms_no_vars lthy' defs); lthy
+  tracing (string_of_thms_no_vars lthy' defs); lthy
 end *}
 
 text {*
@@ -401,7 +401,7 @@
   val intro = 
       prove_ind lthy eo_defs srules cnewpreds ((e_pred, newpred), e_arg_tys)
 in
-  writeln (string_of_thm lthy intro); lthy
+  tracing (string_of_thm lthy intro); lthy
 end *}
 
 text {*
@@ -460,7 +460,7 @@
 let 
   val ind_thms = inds eo_rules eo_defs eo_preds eo_arg_tyss lthy
 in
-  writeln (string_of_thms lthy ind_thms); lthy
+  tracing (string_of_thms lthy ind_thms); lthy
 end *}
 
 
@@ -526,7 +526,7 @@
   val ctrms = [@{cterm \"a::nat\"}, @{cterm \"b::nat\"}, @{cterm \"c::nat\"}]
   val new_thm = all_elims ctrms @{thm all_elims_test}
 in
-  writeln (string_of_thm_no_vars @{context} new_thm)
+  tracing (string_of_thm_no_vars @{context} new_thm)
 end"
   "P a b c"}
 
@@ -542,7 +542,7 @@
 "let
   val res = imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}
 in
-  writeln (string_of_thm_no_vars @{context} res)
+  tracing (string_of_thm_no_vars @{context} res)
 end"
   "C"}
 

--- 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*}

Binary file progtutorial.pdf has changed