--- a/ProgTutorial/Intro.thy	Fri Nov 04 09:29:50 2011 +0000
+++ b/ProgTutorial/Intro.thy	Sat Nov 05 18:44:28 2011 +0000
@@ -214,6 +214,46 @@
   case code maintenance is done for you.
 *}
 
+section {* Serious Isabelle ML-Programming *}
+
+text {*
+  As already pointed out in the previous section, Isabelle is a joint effort 
+  of many developers. Therefore, disruptions that break the work of others
+  are generally frowned upon. ``Accidents'' however do happen and everybody knows
+  this. Still to keep them to a minimum, you can submit your changes first to a rather 
+  sophisticated \emph{testboard}, which will perform checks of your changes agains the
+  Isabelle repository and against the AFP. The advantage of the testboard is
+  that the testing is performed by rather powerful machines, saving you lengthy
+  tests on, for example, your laptop. You can see the results of the testboard 
+  at 
+
+  \begin{isabelle}
+  ??
+  \end{isabelle}
+
+  which is organised like a Mercurial repository. A green point next to a change
+  indicates that the change passes the corresponding tests (for this of course you
+  have to allow some time). To facilitate the use of the testboard you should add 
+
+  \begin{isabelle}
+  \begin{tabular}{@ {}l}
+  @{text "[path]"}\\
+  @{text "testboard = "}
+  \end{tabular}
+  \end{isabelle}
+
+  to your Mercurial settings file. Then you can test any changes using the command
+
+  @{text [display] "$ hg push -f testboard"}
+
+  Note that for pushing changes to the testboard you need to add the option @{text "-f"},
+  which however should \emph{never} be used with the main Isabelle repository. While
+  the testboard is a great system for supporting Isabelle developers, its 
+  disadvantage is that it needs login permissions for the computers in Munich. So in order 
+  to use it, you might have to ask other developers.
+*}
+
+
 section {* Some Naming Conventions in the Isabelle Sources *}
 
 text {*