--- a/ProgTutorial/Intro.thy	Wed Jun 24 15:58:59 2009 +0200
+++ b/ProgTutorial/Intro.thy	Tue Jul 14 01:42:35 2009 +0200
@@ -62,9 +62,14 @@
   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
   often your best friend while programming with Isabelle, or
-  hypersearch if you program using jEdit under MacOSX.
+  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
+  files. The Mercurial repository\footnote{\url{http://isabelle.in.tum.de/repos/isabelle/}} 
+  for Isabelle  provides convenient interfaces to query the history of
+  files and ``change sets''.
   \end{description}
 
+
 *}
 
 section {* Typographic Conventions *}
@@ -119,6 +124,45 @@
   to solve the exercises on your own, and then look at the solutions.
 *}
 
+section {* Aaaaargh! My Code Does not Work Anymore *}
+
+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 
+  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 
+  might be more gratifying. Isabelle is a research project. In most circumstances 
+  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 code, developers are strongly urged to 
+  test against Isabelle's code base. If your project is part of that code base, 
+  then code 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 *}
 
 text {*
@@ -141,12 +185,6 @@
   \end{itemize}
 *}
 
-section {* Aaaaargh! My Code Does not Work Anymore (TBD) *}
-
-text {*
-  
-*}
-
 section {* Acknowledgements *}
 
 text {*