--- a/ProgTutorial/Intro.thy	Tue Jun 14 22:09:40 2011 +0100
+++ b/ProgTutorial/Intro.thy	Fri Jun 17 16:58:05 2011 +0100
@@ -28,8 +28,8 @@
   Isabelle programming, and also explain ``tricks of the trade''. We also hope
   the tutorial will encourage students and researchers to play with Isabelle
   and implement new ideas. The source code of Isabelle can look intimidating,
-  but beginners can get by with knowledge of only a small number of functions
-  and a few basic coding conventions.
+  but beginners can get by with knowledge of only a handful of concepts, 
+  a small number of functions and a few basic coding conventions.
 
 
   The best way to get to know the ML-level of Isabelle is by experimenting
@@ -51,7 +51,11 @@
   the functional programming language ML, the language in which most of
   Isabelle is implemented. If you are unfamiliar with either of these two
   subjects, then you should first work through the Isabelle/HOL tutorial
-  \cite{isa-tutorial} or Paulson's book on ML \cite{paulson-ml2}.
+  \cite{isa-tutorial} or Paulson's book on ML \cite{paulson-ml2}. Recently,
+  Isabelle has adopted a sizable amount of Scala code for a slick GUI
+  based on jEdit. This part of the code is beyond the interest of this
+  tutorial, since it mostly does not concern the regular Isabelle 
+  developer.
 *}
 
 section {* Existing Documentation *}
@@ -80,9 +84,12 @@
   \begin{description}
   \item[The Isabelle sources.] They are the ultimate reference for how
   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. This tutorial contains frequently pointers to the
+  way things are actually implemented. While much of the Isabelle
+  code is uncommented, some parts have very helpful comments---particularly
+  the code about theorems and terms. Despite the lack of comments in most
+  parts, it is often good to look at code that does similar things as you 
+  want to do and 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.\footnote{Or
   hypersearch if you work with jEdit.} To understand the sources,
@@ -148,22 +155,23 @@
 section {* How To Understand Isabelle Code *}
 
 text {*
-  One of the more difficult aspects of any kind of programming is to understand code
-  written by somebody else. This is aggravated in Isabelle by the fact that many parts of
-  the code contain none or 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 distribution. Such
+  One of the more difficult aspects of any kind of programming is to
+  understand code written by somebody else. This is aggravated in Isabelle by
+  the fact that many parts of the code contain none or 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 distribution. 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 effective method
-  for understanding what some piece of 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. And there 
-  seems to be no better way for understanding code in Isabelle.
+  for understanding what some piece of code is doing. However do not expect
+  quick results with this! It is painful. Depending on the size of the code
+  you are looking at, you will spend the better part of a quiet afternoon with
+  it. And there seems to be no better way for understanding code in Isabelle.
 *}