diff -r f286dfa9f173 -r 2728e8daebc0 ProgTutorial/FirstSteps.thy
--- 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