--- a/ProgTutorial/Intro.thy	Wed Apr 07 11:32:00 2010 +0200
+++ b/ProgTutorial/Intro.thy	Sat Apr 24 22:55:50 2010 +0200
@@ -145,6 +145,28 @@
   to solve the exercises on your own, and then look at the solutions.
 *}
 
+section {* How To Understand Code in Isabelle *}
+
+text {*
+  One of the more difficult aspects of programming is to understand somebody
+  else's code. This is aggravated in Isabelle by the fact that many parts of
+  the code contain only few comments. There is one strategy that might be
+  helpful to navigate your way: ML is an interactive programming environment,
+  which means you can evaluate code on the fly (for example inside an
+  \isacommand{ML}~@{text "\<verbopen>\<dots>\<verbclose>"} section). So you can copy
+  self-contained chunks of existing code into a separate theory file and then
+  study it alongside with examples. You can also install probes inside the
+  copied code without having to recompile the whole Isabelle distributions. Such
+  probes might be messages or printouts of variables (see chapter
+  \ref{chp:firststeps}). Although PolyML also contains a debugger, it seems
+  probing the code with explicit print statements is the most efficient method
+  for understanding what some code is doing. However do not expect quick
+  results with this! Depending on the size of the code you are looking at, 
+  you will spend the better part of a quiet afternoon with it. But there 
+  seems to be no better way around it.
+*}
+
+
 section {* Aaaaargh! My Code Does not Work Anymore *}
 
 text {*
@@ -248,7 +270,10 @@
   Please let me know of any omissions. Responsibility for any remaining
   errors lies with me.\bigskip
 
-  \vspace{5cm}
+  \newpage
+  \mbox{}\\[5cm]
+  
+  
   {\Large\bf
   This tutorial is still in the process of being written! All of the
   text is still under construction. Sections and