--- a/ProgTutorial/FirstSteps.thy	Sat Oct 03 13:01:39 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Sat Oct 03 19:10:23 2009 +0200
@@ -120,7 +120,7 @@
   to track down errors.
 *}
 
-section {* Debugging and Printing\label{sec:printing} *}
+section {* Printing and Debugging\label{sec:printing} *}
 
 text {*
   During development you might find it necessary to inspect some data in your
@@ -211,7 +211,7 @@
   thm}. Isabelle contains elaborate pretty-printing functions for printing
   them (see Section \ref{sec:pretty}), but for quick-and-dirty solutions they
   are a bit unwieldy. One way to transform a term into a string is to use the
-  function @{ML_ind  string_of_term in Syntax} in structure @{ML_struct
+  function @{ML_ind  string_of_term in Syntax} in the structure @{ML_struct
   Syntax}, which we bind for more convenience to the toplevel.
 *}
 
@@ -635,7 +635,7 @@
   together. We have already seen such plumbing in the function @{ML
   apply_fresh_args}, where @{ML curry} is needed for making the function @{ML
   list_comb} that works over pairs to fit with the combinator @{ML "|>"}. Such 
-  plumbing is also needed in situations where a functions operate over lists, 
+  plumbing is also needed in situations where a function operate over lists, 
   but one calculates only with a single element. An example is the function 
   @{ML_ind  check_terms in Syntax}, whose purpose is to type-check a list 
   of terms.
@@ -653,8 +653,8 @@
 *}
 
 text {*
-  In this example we obtain three terms in which @{text m} and @{text n} are of
-  type @{typ "nat"}. If you have only a single term, then @{ML
+  In this example we obtain three terms whose variables @{text m} and @{text
+  n} are of type @{typ "nat"}. If you have only a single term, then @{ML
   check_terms in Syntax} needs plumbing. This can be done with the function
   @{ML singleton}.\footnote{There is already a function @{ML check_term in
   Syntax} in the Isabelle sources that is defined in terms of @{ML singleton}
@@ -713,7 +713,7 @@
   the function @{ML_ind  theory_name in Context}. 
 
   Note, however, that antiquotations are statically linked, that is their value is
-  determined at ``compile-time'', not ``run-time''. For example the function
+  determined at ``compile-time'', not at ``run-time''. For example the function
 *}
 
 ML{*fun not_current_thyname () = Context.theory_name @{theory} *}
@@ -743,7 +743,7 @@
   The point of these antiquotations is that referring to theorems in this way
   makes your code independent from what theorems the user might have stored
   under this name (this becomes especially important when you deal with
-  theorem lists; see Section \ref{sec:attributes}).
+  theorem lists; see Section \ref{sec:storing}).
 
   You can also refer to the current simpset via an antiquotation. To illustrate 
   this we implement the function that extracts the theorem names stored in a 
@@ -784,7 +784,7 @@
   @{ML_ind  define in LocalTheory}.  This function is used below to define 
   the constant @{term "TrueConj"} as the conjunction @{term "True \<and> True"}.
 *}
-  
+
 local_setup %gray {* 
   LocalTheory.define Thm.internalK 
     ((@{binding "TrueConj"}, NoSyn), 
@@ -798,9 +798,16 @@
   @{text "> "}~@{thm TrueConj_def}
   \end{isabelle}
 
+  \begin{readmore}
+  The basic operations on bindings are implemented in 
+  @{ML_file "Pure/General/binding.ML"}.
+  \end{readmore}
+
   \footnote{\bf FIXME give a better example why bindings are important; maybe
   give a pointer to \isacommand{local\_setup}; if not, then explain
   why @{ML snd} is needed.}
+  \footnote{\bf FIXME: There should probably a separate section on binding, long-names
+  and sign.}
 
   It is also possible to define your own antiquotations. But you should
   exercise care when introducing new ones, as they can also make your code
@@ -1016,13 +1023,14 @@
   "WrongRefData.get @{theory}"
   "ref []"}
 
-  For updating the reference we use the following function.
+  For updating the reference we use the following function
 *}
 
 ML{*fun ref_update n = WrongRefData.map 
       (fn r => let val _ = r := n::(!r) in r end)*}
 
 text {*
+  which takes an integer and adds it to the content of the reference.
   As above we update the reference with the command 
   \isacommand{setup}. 
 *}
@@ -1051,7 +1059,7 @@
 
   Now imagine how often you go backwards and forwards in your proof scripts. 
   By using references in Isabelle code, you are bound to cause all
-  hell to break lose. Therefore observe the coding convention: 
+  hell to break loose. Therefore observe the coding convention: 
   Do not use references for storing data!
 
   \begin{readmore}
@@ -1062,46 +1070,6 @@
   tables and symtables in @{ML_file "Pure/General/table.ML"}.
   \end{readmore}
 
-  A special instance of the data storage mechanism described above are
-  configuration values. They are used to enable users to configure tools
-  without having to resort to the ML-level (and also to avoid
-  references). Assume you want the user to control three values, say @{text
-  bval} containing a boolean, @{text ival} containing an integer and @{text
-  sval} containing a string. These values can be declared by
-*}
-
-ML{*val (bval, setup_bval) = Attrib.config_bool "bval" false
-val (ival, setup_ival) = Attrib.config_int "ival" 0
-val (sval, setup_sval) = Attrib.config_string "sval" "some string" *}
-
-text {* 
-  where each value needs to be given a default. To enable these values, they need to 
-  be set up with
-*}
-
-setup %gray {* 
-  setup_bval #> 
-  setup_ival 
-*}
-
-text {*
-  The user can now manipulate the values from the user-level of Isabelle 
-  with the command
-*}
-
-declare [[bval = true, ival = 3]]
-
-text {*
-  On the ML-level these values can be retrieved using the 
-  function @{ML Config.get}.
-
-  @{ML_response [display,gray] "Config.get @{context} bval" "true"}
-
-  \begin{readmore}
-  For more information about configuration values see 
-  @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}.
-  \end{readmore}
-
   Storing data in a proof context is done in a similar fashion. The
   corresponding functor is @{ML_funct_ind ProofDataFun}. With the 
   following code we can store a list of terms in a proof context. 
@@ -1155,9 +1123,112 @@
   theory. Once we throw away the contexts, we have no access to their
   associated data. This is different to theories, where the command 
   \isacommand{setup} registers the data with the current and future 
-  theories, and therefore can access the data potentially indefinitely. 
+  theories, and therefore can access the data potentially 
+  indefinitely.\footnote{\bf FIXME: check this; it seems that is in
+  conflict with the statements below.} 
+
+  \footnote{\bf FIXME: Say something about generic contexts.}
+
+  There are two special instances of the data storage mechanism described 
+  above. The first instance are named theorem lists. Since storing theorems in a list 
+  is such a common task, there is the special functor @{ML_funct_ind Named_Thms}. 
+  To obtain a named theorem list, you just declare
+*}
+
+ML{*structure FooRules = Named_Thms
+  (val name = "foo" 
+   val description = "Theorems for foo") *}
+
+text {*
+  and set up the @{ML_struct FooRules} with the command
+*}
+
+setup %gray {* FooRules.setup *}
+
+text {*
+  This code declares a data container where the theorems are stored,
+  an attribute @{text foo} (with the @{text add} and @{text del} options
+  for adding and deleting theorems) and an internal ML-interface to retrieve and 
+  modify the theorems.
+
+  Furthermore, the facts are made available on the user-level under the dynamic 
+  fact name @{text foo}. For example you can declare three lemmas to be of the kind
+  @{text foo} by:
 *}
 
+lemma rule1[foo]: "A" sorry
+lemma rule2[foo]: "B" sorry
+lemma rule3[foo]: "C" sorry
+
+text {* and undeclare the first one by: *}
+
+declare rule1[foo del]
+
+text {* and query the remaining ones with:
+
+  \begin{isabelle}
+  \isacommand{thm}~@{text "foo"}\\
+  @{text "> ?C"}\\
+  @{text "> ?B"}
+  \end{isabelle}
+
+  On the ML-level, we can add theorems to the list with @{ML FooRules.add_thm}:
+*} 
+
+setup %gray {* 
+  Context.theory_map (FooRules.add_thm @{thm TrueI}) 
+*}
+
+text {*
+  The rules in the list can be retrieved using the function 
+  @{ML FooRules.get}:
+
+  @{ML_response_fake [display,gray] "FooRules.get @{context}" "[\"True\", \"?C\",\"?B\"]"}
+
+  \begin{readmore}
+  For more information see @{ML_file "Pure/Tools/named_thms.ML"}.
+  \end{readmore}
+
+  The second special instance of the data storage mechanism are configuration
+  values. They are used to enable users to configure tools without having to
+  resort to the ML-level (and also to avoid references). Assume you want the
+  user to control three values, say @{text bval} containing a boolean, @{text
+  ival} containing an integer and @{text sval} containing a string. These
+  values can be declared by
+*}
+
+ML{*val (bval, setup_bval) = Attrib.config_bool "bval" false
+val (ival, setup_ival) = Attrib.config_int "ival" 0
+val (sval, setup_sval) = Attrib.config_string "sval" "some string" *}
+
+text {* 
+  where each value needs to be given a default. To enable these values, they need to 
+  be set up with
+*}
+
+setup %gray {* 
+  setup_bval #> 
+  setup_ival 
+*}
+
+text {*
+  The user can now manipulate the values from the user-level of Isabelle 
+  with the command
+*}
+
+declare [[bval = true, ival = 3]]
+
+text {*
+  On the ML-level these values can be retrieved using the 
+  function @{ML Config.get}.
+
+  @{ML_response [display,gray] "Config.get @{context} bval" "true"}
+
+  \begin{readmore}
+  For more information about configuration values see 
+  @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}.
+  \end{readmore}
+*}
 
 
 (**************************************************)

--- a/ProgTutorial/General.thy	Sat Oct 03 13:01:39 2009 +0200
+++ b/ProgTutorial/General.thy	Sat Oct 03 19:10:23 2009 +0200
@@ -7,7 +7,8 @@
 text {*
   Isabelle is build around a few central ideas. One is the LCF-approach to
   theorem proving where there is a small trusted core and everything else is
-  build on top of this trusted core.
+  build on top of this trusted core. The central data structures involved
+  in this core are certified terms and types as well as theorems.
 
 *}
 
@@ -15,8 +16,9 @@
 section {* Terms and Types *}
 
 text {*
-  One way to construct Isabelle terms, is by using the antiquotation 
-  \mbox{@{text "@{term \<dots>}"}}. For example
+  In Isabelle there are certified terms (respectively types) and uncertified
+  terms. The latter are called just terms. One way to construct them is by 
+  using the antiquotation \mbox{@{text "@{term \<dots>}"}}. For example
 
   @{ML_response [display,gray] 
 "@{term \"(a::nat) + b = c\"}" 
@@ -446,7 +448,8 @@
   @{ML_response [display,gray]
   "@{type_name \"list\"}" "\"List.list\""}
 
-  (FIXME: Explain the following better.)
+  \footnote{\bf FIXME: Explain the following better; maybe put in a separate
+  section and link with the comment in the antiquotation section.}
 
   Occasionally you have to calculate what the ``base'' name of a given
   constant is. For this you can use the function @{ML_ind  "Sign.extern_const"} or
@@ -537,9 +540,9 @@
   number representing their sum.
   \end{exercise}
 
-  \begin{exercise}\footnote{Personal communication of
-  de Bruijn to Dyckhoff.}\label{ex:debruijn}
-  Implement the function, which we below name deBruijn, that depends on a natural
+  \begin{exercise}\label{ex:debruijn}
+  Implement the function, which we below name deBruijn\footnote{According to 
+  personal communication of de Bruijn to Dyckhoff.}, that depends on a natural
   number n$>$0 and constructs terms of the form:
   
   \begin{center}
@@ -551,7 +554,7 @@
   \end{tabular}
   \end{center}
 
-  For n=3 this function returns the term
+  This function returns for n=3 the term
 
   \begin{center}
   \begin{tabular}{l}
@@ -685,13 +688,13 @@
   @{ML_file "Pure/type_infer.ML"}. 
   \end{readmore}
 
-  (FIXME: say something about sorts)
+  \footnote{\bf FIXME: say something about sorts.}
 
   \begin{exercise}
   Check that the function defined in Exercise~\ref{fun:revsum} returns a
   result that type-checks. See what happens to the  solutions of this 
-  exercise given in \ref{ch:solutions} when they receive an ill-typed term
-  as input.
+  exercise given in Appendix \ref{ch:solutions} when they receive an 
+  ill-typed term as input.
   \end{exercise}
 *}
 
@@ -982,7 +985,7 @@
   
   However, here also a weakness of the concept
   of theorem attributes shows through: since theorem attributes can be
-  arbitrary functions, they do not in general commute. If you try
+  arbitrary functions, they do not commute in general. If you try
 
   \begin{isabelle}
   \isacommand{thm}~@{text "test[MY_THEN eq_reflection, my_sym]"}\\
@@ -992,56 +995,34 @@
   you get an exception indicating that the theorem @{thm [source] sym}
   does not resolve with meta-equations. 
 
-  The purpose of @{ML_ind  rule_attribute in Thm} is to directly manipulate theorems.
-  Another usage of theorem attributes is to add and delete theorems from stored data.
-  For example the theorem attribute @{text "[simp]"} adds or deletes a theorem from the
-  current simpset. For these applications, you can use @{ML_ind  declaration_attribute in Thm}. 
-  To illustrate this function, let us introduce a reference containing a list
-  of theorems.
-*}
-
-ML{*val my_thms = Unsynchronized.ref ([] : thm list)*}
-
-text {* 
-  The purpose of this reference is to store a list of theorems.
-  We are going to modify it by adding and deleting theorems.
-  However, a word of warning: such references must not 
-  be used in any code that is meant to be more than just for testing purposes! 
-  Here it is only used to illustrate matters. We will show later how to store 
-  data properly without using references.
- 
-  We need to provide two functions that add and delete theorems from this list. 
-  For this we use the two functions:
+  The purpose of @{ML_ind rule_attribute in Thm} is to directly manipulate
+  theorems.  Another usage of theorem attributes is to add and delete theorems
+  from stored data.  For example the theorem attribute @{text "[simp]"} adds
+  or deletes a theorem from the current simpset. For these applications, you
+  can use @{ML_ind declaration_attribute in Thm}. To illustrate this function,
+  let us introduce a theorem list.
 *}
 
-ML{*fun my_thm_add thm ctxt =
-  (my_thms := Thm.add_thm thm (!my_thms); ctxt)
-
-fun my_thm_del thm ctxt =
-  (my_thms := Thm.del_thm thm (!my_thms); ctxt)*}
+ML{*structure MyThms = Named_Thms
+  (val name = "attr_thms" 
+   val description = "Theorems for an Attribute") *}
 
-text {*
-  These functions take a theorem and a context and, for what we are explaining
-  here it is sufficient that they just return the context unchanged. They change
-  however the reference @{ML my_thms}, whereby the function 
-  @{ML_ind  add_thm in Thm} adds a theorem if it is not already included in 
-  the list, and @{ML_ind  del_thm in Thm} deletes one (both functions use the 
-  predicate @{ML_ind  eq_thm_prop in Thm}, which compares theorems according to 
-  their proved propositions modulo alpha-equivalence).
-
-  You can turn functions @{ML my_thm_add} and @{ML my_thm_del} into 
-  attributes with the code
+text {* 
+  We are going to modify this list by adding and deleting theorems.
+  For this we use the two functions @{ML MyThms.add_thm} and
+  @{ML MyThms.del_thm}. You can turn them into attributes 
+  with the code
 *}
 
-ML{*val my_add = Thm.declaration_attribute my_thm_add
-val my_del = Thm.declaration_attribute my_thm_del *}
+ML{*val my_add = Thm.declaration_attribute MyThms.add_thm
+val my_del = Thm.declaration_attribute MyThms.del_thm *}
 
 text {* 
   and set up the attributes as follows
 *}
 
 attribute_setup %gray my_thms = {* Attrib.add_del my_add my_del *} 
-  "maintaining a list of my_thms - rough test only!" 
+  "maintaining a list of my_thms" 
 
 text {*
   The parser @{ML_ind  add_del in Attrib} is a predefined parser for 
@@ -1055,12 +1036,13 @@
   then you can see it is added to the initially empty list.
 
   @{ML_response_fake [display,gray]
-  "!my_thms" "[\"True\"]"}
+  "MyThms.get @{context}" 
+  "[\"True\"]"}
 
   You can also add theorems using the command \isacommand{declare}.
 *}
 
-declare test[my_thms] trueI_2[my_thms add] 
+declare test[my_thms] trueI_2[my_thms add]
 
 text {*
   With this attribute, the @{text "add"} operation is the default and does 
@@ -1068,7 +1050,7 @@
   theorem list to be updated as:
 
   @{ML_response_fake [display,gray]
-  "!my_thms"
+  "MyThms.get @{context}"
   "[\"True\", \"Suc (Suc 0) = 2\"]"}
 
   The theorem @{thm [source] trueI_2} only appears once, since the 
@@ -1081,144 +1063,14 @@
 text {* After this, the theorem list is again: 
 
   @{ML_response_fake [display,gray]
-  "!my_thms"
+  "MyThms.get @{context}"
   "[\"True\"]"}
 
-  We used in this example two functions declared as @{ML_ind  declaration_attribute in Thm}, 
-  but there can be any number of them. We just have to change the parser for reading
-  the arguments accordingly. 
-
-  However, as said at the beginning of this example, using references for storing theorems is
-  \emph{not} the received way of doing such things. The received way is to 
-  start a ``data slot'', below called @{text MyThmsData}, generated by the functor 
-  @{text GenericDataFun}:
-*}
-
-ML{*structure MyThmsData = GenericDataFun
- (type T = thm list
-  val empty = []
-  val extend = I
-  fun merge _ = Thm.merge_thms) *}
-
-text {*
-  The type @{text "T"} of this data slot is @{ML_type "thm list"}.\footnote{FIXME: give a pointer
-  to where data slots are explained properly.}
-  To use this data slot, you only have to change @{ML my_thm_add} and
-  @{ML my_thm_del} to:
-*}
-
-ML{*val my_thm_add = MyThmsData.map o Thm.add_thm
-val my_thm_del = MyThmsData.map o Thm.del_thm*}
-
-text {*
-  where @{ML MyThmsData.map} updates the data appropriately. The
-  corresponding theorem attributes are
-*}
-
-ML{*val my_add = Thm.declaration_attribute my_thm_add
-val my_del = Thm.declaration_attribute my_thm_del *}
-
-text {*
-  and the setup is as follows
-*}
-
-attribute_setup %gray my_thms2 = {* Attrib.add_del my_add my_del *} 
-  "properly maintaining a list of my_thms"
-
-text {*
-  Initially, the data slot is empty 
-
-  @{ML_response_fake [display,gray]
-  "MyThmsData.get (Context.Proof @{context})"
-  "[]"}
-
-  but if you prove
-*}
-
-lemma three[my_thms2]: "3 = Suc (Suc (Suc 0))" by simp
-
-text {*
-  then the lemma is recorded. 
-
-  @{ML_response_fake [display,gray]
-  "MyThmsData.get (Context.Proof @{context})"
-  "[\"3 = Suc (Suc (Suc 0))\"]"}
-
-  With theorem attribute @{text my_thms2} you can also nicely see why it 
-  is important to 
-  store data in a ``data slot'' and \emph{not} in a reference. Backtrack
-  to the point just before the lemma @{thm [source] three} was proved and 
-  check the the content of @{ML_struct MyThmsData}: it should be empty. 
-  The addition has been properly retracted. Now consider the proof:
-*}
+  We used in this example two functions declared as @{ML_ind
+  declaration_attribute in Thm}, but there can be any number of them. We just
+  have to change the parser for reading the arguments accordingly.
 
-lemma four[my_thms]: "4 = Suc (Suc (Suc (Suc 0)))" by simp
-
-text {*
-  Checking the content of @{ML my_thms} gives
-
-  @{ML_response_fake [display,gray]
-  "!my_thms"
-  "[\"4 = Suc (Suc (Suc (Suc 0)))\", \"True\"]"}
-
-  as expected, but if you backtrack before the lemma @{thm [source] four}, the
-  content of @{ML my_thms} is unchanged. The backtracking mechanism
-  of Isabelle is completely oblivious about what to do with references, but
-  properly treats ``data slots''!
-
-  Since storing theorems in a list is such a common task, there is the special
-  functor @{ML_functor Named_Thms}, which does most of the work for you. To obtain
-  a named theorem list, you just declare
-*}
-
-ML{*structure FooRules = Named_Thms
- (val name = "foo" 
-  val description = "Rules for foo") *}
-
-text {*
-  and set up the @{ML_struct FooRules} with the command
-*}
-
-setup %gray {* FooRules.setup *}
-
-text {*
-  This code declares a data slot where the theorems are stored,
-  an attribute @{text foo} (with the @{text add} and @{text del} options
-  for adding and deleting theorems) and an internal ML interface to retrieve and 
-  modify the theorems.
-
-  Furthermore, the facts are made available on the user-level under the dynamic 
-  fact name @{text foo}. For example you can declare three lemmas to be of the kind
-  @{text foo} by:
-*}
-
-lemma rule1[foo]: "A" sorry
-lemma rule2[foo]: "B" sorry
-lemma rule3[foo]: "C" sorry
-
-text {* and undeclare the first one by: *}
-
-declare rule1[foo del]
-
-text {* and query the remaining ones with:
-
-  \begin{isabelle}
-  \isacommand{thm}~@{text "foo"}\\
-  @{text "> ?C"}\\
-  @{text "> ?B"}
-  \end{isabelle}
-
-  On the ML-level the rules marked with @{text "foo"} can be retrieved
-  using the function @{ML FooRules.get}:
-
-  @{ML_response_fake [display,gray] "FooRules.get @{context}" "[\"?C\",\"?B\"]"}
-
-  \begin{readmore}
-  For more information see @{ML_file "Pure/Tools/named_thms.ML"}.
-  \end{readmore}
-
-  (FIXME What are: @{text "theory_attributes"}, @{text "proof_attributes"}?)
-
+  \footnote{\bf FIXME What are: @{text "theory_attributes"}, @{text "proof_attributes"}?}
 
   \begin{readmore}
   FIXME: @{ML_file "Pure/more_thm.ML"}; parsers for attributes is in 

--- a/ProgTutorial/Intro.thy	Sat Oct 03 13:01:39 2009 +0200
+++ b/ProgTutorial/Intro.thy	Sat Oct 03 19:10:23 2009 +0200
@@ -36,7 +36,7 @@
   writing theories and proofs. We also assume that readers are familiar with
   the functional programming language ML, the language in which most of
   Isabelle is implemented. If you are unfamiliar with either of these two
-  subjects, you should first work through the Isabelle/HOL tutorial
+  subjects, then you should first work through the Isabelle/HOL tutorial
   \cite{isa-tutorial} or Paulson's book on ML \cite{paulson-ml2}.
 *}
 
@@ -68,7 +68,8 @@
   things really work. Therefore you should not hesitate to look at the
   way things are actually implemented. More importantly, it is often
   good to look at code that does similar things as you want to do and
-  learn from it. The UNIX command \mbox{@{text "grep -R"}} is
+  learn from it. This tutorial contains frequently pointers to the
+  Isabelle sources. Still, the UNIX command \mbox{@{text "grep -R"}} is
   often your best friend while programming with Isabelle, or
   hypersearch if you program using jEdit under MacOSX. To understand the sources,
   it is often also necessary to track the change history of a file or
@@ -82,7 +83,7 @@
 
 text {*
   All ML-code in this tutorial is typeset in shaded boxes, like the following 
-  ML-expression:
+  simple ML-expression:
 
   \begin{isabelle}
   \begin{graybox}
@@ -133,7 +134,7 @@
 
 text {*
   One unpleasant aspect of any code development inside a larger system is that
-  one has to aim at a ``moving target''. The Isabelle system is no exception. Every 
+  one has to aim at a ``moving target''. Isabelle 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 
@@ -141,31 +142,31 @@
   it is just impossible to make research backward compatible (imagine Darwin 
   attempting to make the Theory of Evolution backward compatible).
 
-  However, there are a few steps you can take to mitigate unwanted interferences
-  with code changes from other developers. First, you can base your code on the latest 
-  stable release of Isabelle (it is aimed to have one such release at least 
-  once every year). This 
-  might cut you off from the latest feature
-  implemented in Isabelle, but at least you do not have to track side-steps
-  or dead-ends in the Isabelle development. Of course this means also you have
-  to synchronise your code at the next stable release. Another possibility
-  is to get your code into the Isabelle distribution. For this you have
-  to convince other developers that your code or project is of general interest. 
-  If you managed to do this, then the problem of the moving target goes 
-  away, because when checking in new code, developers are strongly urged to 
-  test it against Isabelle's code base. If your project is part of that code base, 
-  then maintenance is done by others. Unfortunately, this might not
-  be a helpful advice for all types of projects. A lower threshold for inclusion has the 
-  Archive of Formalised Proofs, short AFP.\footnote{\url{http://afp.sourceforge.net/}}
-  This archive has been created mainly for formalisations that are
-  interesting but not necessarily of general interest. If you have ML-code as
-  part of a formalisation, then this might be the right place for you. There
-  is no problem with updating your code after submission. At the moment
-  developers are not as diligent with checking their code against the AFP than
-  with checking agains the distribution, but generally problems will be caught
-  and the developer, who caused them, is expected to fix them. So also
-  in this case code maintenance is done for you. 
-
+  However, there are a few steps you can take to mitigate unwanted
+  interferences with code changes from other developers. First, you can base
+  your code on the latest stable release of Isabelle (it is aimed to have one
+  such release at least once every year). This might cut you off from the
+  latest feature implemented in Isabelle, but at least you do not have to
+  track side-steps or dead-ends in the Isabelle development. Of course this
+  means also you have to synchronise your code at the next stable release. If
+  you do not synchronise, be warned that code seems to ``rot'' very
+  quickly. Another possibility is to get your code into the Isabelle
+  distribution. For this you have to convince other developers that your code
+  or project is of general interest. If you managed to do this, then the
+  problem of the moving target goes away, because when checking in new code,
+  developers are strongly urged to test it against Isabelle's code base. If
+  your project is part of that code base, then maintenance is done by
+  others. Unfortunately, this might not be a helpful advice for all types of
+  projects. A lower threshold for inclusion has the Archive of Formalised
+  Proofs, short AFP.\footnote{\url{http://afp.sourceforge.net/}} This archive
+  has been created mainly for formalisations that are interesting but not
+  necessarily of general interest. If you have ML-code as part of a
+  formalisation, then this might be the right place for you. There is no
+  problem with updating your code after submission. At the moment developers
+  are not as diligent with checking their code against the AFP than with
+  checking agains the distribution, but generally problems will be caught and
+  the developer, who caused them, is expected to fix them. So also in this
+  case code maintenance is done for you.
 *}
 
 section {* Some Naming Conventions in the Isabelle Sources *}
@@ -208,7 +209,7 @@
 
   \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout}, 
   \ref{rec:external} and \ref{rec:oracle}. He also wrote section \ref{sec:conversion} 
-  and helped with recipe \ref{rec:timing}. Parts of the section \ref{sec:storing}
+  and helped with recipe \ref{rec:timing}. Parts of section \ref{sec:storing}
   are by him.
 
   \item {\bf Jeremy Dawson} wrote the first version of the chapter

--- a/ProgTutorial/Package/Ind_Code.thy	Sat Oct 03 13:01:39 2009 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy	Sat Oct 03 19:10:23 2009 +0200
@@ -117,7 +117,7 @@
 let
   val def = defn_aux lthy eo_orules eo_preds (e_pred, e_arg_tys)
 in
-  tracing (Syntax.string_of_term lthy def); lthy
+  tracing (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
-  tracing (Syntax.string_of_term lthy def); lthy
+  tracing (string_of_term lthy def); lthy
 end *}
 
 

--- a/ProgTutorial/ROOT.ML	Sat Oct 03 13:01:39 2009 +0200
+++ b/ProgTutorial/ROOT.ML	Sat Oct 03 19:10:23 2009 +0200
@@ -6,6 +6,8 @@
 use_thy "Intro";
 use_thy "FirstSteps";
 use_thy "General";
+
+no_document use_thy "Helper/Command/Command";
 use_thy "Parsing";
 use_thy "Tactical";
 

--- a/ProgTutorial/Recipes/Sat.thy	Sat Oct 03 13:01:39 2009 +0200
+++ b/ProgTutorial/Recipes/Sat.thy	Sat Oct 03 19:10:23 2009 +0200
@@ -1,6 +1,6 @@
 
 theory Sat
-imports Main "../Base"
+imports Main "../FirstSteps"
 begin
 
 section {* SAT Solvers\label{rec:sat} *}
@@ -59,7 +59,7 @@
   @{ML table'} is:
 
   @{ML_response_fake [display,gray]
-  "map (apfst (Syntax.string_of_term @{context})) (Termtab.dest table')"
+  "map (apfst (string_of_term @{context})) (Termtab.dest table')"
   "(\<forall>x. P x, 1)"}
   
   In the print out of the tabel, we used some pretty printing scaffolding 

--- a/ProgTutorial/Solutions.thy	Sat Oct 03 13:01:39 2009 +0200
+++ b/ProgTutorial/Solutions.thy	Sat Oct 03 19:10:23 2009 +0200
@@ -1,5 +1,5 @@
 theory Solutions
-imports Base "Recipes/Timing"
+imports FirstSteps "Recipes/Timing"
 begin
 
 chapter {* Solutions to Most Exercises\label{ch:solutions} *}
@@ -288,7 +288,7 @@
   This function generates for example:
 
   @{ML_response_fake [display,gray] 
-  "writeln (Syntax.string_of_term @{context} (term_tree 2))" 
+  "writeln (string_of_term @{context} (term_tree 2))" 
   "(1 + 2) + (3 + 4)"} 
 
   The next function constructs a goal of the form @{text "P \<dots>"} with a term 

--- a/ProgTutorial/Tactical.thy	Sat Oct 03 13:01:39 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Sat Oct 03 19:10:23 2009 +0200
@@ -1655,7 +1655,7 @@
 ML{*fun fail_simproc' simpset redex = 
 let
   val ctxt = Simplifier.the_context simpset
-  val _ = tracing ("The redex: " ^ (Syntax.string_of_term ctxt redex))
+  val _ = tracing ("The redex: " ^ (string_of_term ctxt redex))
 in
   NONE
 end*}

--- a/ProgTutorial/document/root.tex	Sat Oct 03 13:01:39 2009 +0200
+++ b/ProgTutorial/document/root.tex	Sat Oct 03 19:10:23 2009 +0200
@@ -57,6 +57,8 @@
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % for exercises, comments and readmores
+\newtheoremstyle{exercisestyle}{\topsep}{\topsep}{\small\it}{}{\small\bfseries}{:}{1ex}{}
+\theoremstyle{exercisestyle}
 \newtheorem{exercise}{Exercise}[section]
 \newcommand{\solution}[1]{{\bf Solution for Exercise~\ref{#1}.}}
 

Binary file progtutorial.pdf has changed