--- a/ProgTutorial/Base.thy	Tue Jul 14 01:42:35 2009 +0200
+++ b/ProgTutorial/Base.thy	Tue Jul 14 16:34:24 2009 +0200
@@ -1,5 +1,5 @@
 theory Base
-imports Main
+imports Main LaTeXsugar
 uses
   "output_tutorial.ML"
   "chunks.ML"
@@ -11,17 +11,17 @@
 
 fun propagate_env (context as Context.Proof lthy) =
       Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy)
-  | propagate_env context = context;
+  | propagate_env context = context
 
 fun propagate_env_prf prf = Proof.map_contexts
-  (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf;
+  (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf
 
 val _ =
   OuterSyntax.command "ML" "eval ML text within theory"
     (OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl)
     (OuterParse.ML_source >> (fn (txt, pos) =>
       Toplevel.generic_theory
-        (ML_Context.exec (fn () => ML_Context.eval true pos txt) #> propagate_env)));
+        (ML_Context.exec (fn () => ML_Context.eval true pos txt) #> propagate_env)))
 
 val _ =
   OuterSyntax.command "ML_prf" "ML text within proof" 
@@ -33,7 +33,7 @@
 val _ =
   OuterSyntax.command "ML_val" "diagnostic ML text" 
   (OuterKeyword.tag "TutorialML" OuterKeyword.diag)
-    (OuterParse.ML_source >> IsarCmd.ml_diag true);
+    (OuterParse.ML_source >> IsarCmd.ml_diag true)
 
 *}
 

--- a/ProgTutorial/FirstSteps.thy	Tue Jul 14 01:42:35 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Tue Jul 14 16:34:24 2009 +0200
@@ -57,7 +57,8 @@
   code, rather they indicate what the response is when the code is evaluated.
   There are also the commands \isacommand{ML\_val} and \isacommand{ML\_prf} for
   including ML-code. The first evaluates the given code, but any effect on the 
-  `ambient' theory is suppressed. The second needs to be used if ML-code is defined 
+  theory, in which the code is embedded, is suppressed. The second needs to 
+  be used if ML-code is defined 
   inside a proof. For example
 
   \begin{quote}
@@ -70,7 +71,7 @@
   \end{quote}
 
   However, both commands will only play minor roles in this tutorial (we will always 
-  arrange that the ML-code is defined outside of proofs).
+  arrange that the ML-code is defined outside of proofs, for example).
 
   Once a portion of code is relatively stable, you usually want to export it
   to a separate ML-file. Such files can then be included somewhere inside a 
@@ -103,7 +104,7 @@
   \end{quote}
 
   Note that no parentheses are given this time. Note also that the 
-  `used' file should not contain any
+  included ML-file should not contain any
   \isacommand{use} itself. Otherwise Isabelle is unable to record all
   file dependencies, which is a nuisance if you have to track down
   errors.
@@ -634,21 +635,18 @@
   kinds of logical elements from the ML-level.
 *}
 
-text {* FIXME: an example of a user defined antiquotation *}
+text {* FIXME: give an example of a user defined antiquotation *}
 
 ML{*ML_Antiquote.inline "term_pat"
   (Args.context -- Scan.lift Args.name_source >>
      (fn (ctxt, s) =>
-       let 
-         val t = ProofContext.read_term_pattern ctxt s
-       in 
-         ML_Syntax.atomic (ML_Syntax.print_term t) 
-       end))*}
+       s |> ProofContext.read_term_pattern ctxt
+         |> ML_Syntax.print_term
+         |> ML_Syntax.atomic))*}
 
 ML{*@{term_pat "?x + ?y"}*}
 
 text {*
-
   \begin{readmore}
   @{ML_file "Pure/ML/ml_antiquote.ML"}
   \end{readmore}

--- a/ProgTutorial/Intro.thy	Tue Jul 14 01:42:35 2009 +0200
+++ b/ProgTutorial/Intro.thy	Tue Jul 14 16:34:24 2009 +0200
@@ -128,7 +128,7 @@
 
 text {*
   One unpleasant aspect of any code development inside a larger system is that
-  one has to aim for a ``moving target''. The Isabelle system is no exception. Every 
+  one has to aim at a ``moving target''. The Isabelle system is no exception. Every 
   update lets potentially all hell break loose, because other developers have
   changed code you are relying on. Cursing is somewhat helpful in such situations, 
   but taking the view that incompatible code changes are a fact of life 
@@ -195,7 +195,7 @@
   \begin{itemize}
   \item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the
   \simpleinductive-package and the code for the @{text
-  "chunk"}-antiquotation. He also wrote the first version of the chapter
+  "chunk"}-antiquotation. He also wrote the first version of this chapter
   describing the package and has been helpful \emph{beyond measure} with
   answering questions about Isabelle.
 

Binary file progtutorial.pdf has changed