--- a/ProgTutorial/Advanced.thy	Wed Dec 02 03:46:32 2009 +0100
+++ b/ProgTutorial/Advanced.thy	Wed Dec 02 17:06:41 2009 +0100
@@ -16,14 +16,14 @@
 text {*
   While terms, types and theorems are the most basic data structures in
   Isabelle, there are a number of layers built on top of them. Most of these
-  layers are concerned with storing and manipulating data. Handling
-  them properly is an essential skill for Isabelle programming. The most basic
-  layer are theories. They contain global data and can be seen as the
-  ``long-term memory'' of Isabelle. There is usually only one theory
-  active at each moment. Proof contexts and local theories, on the
+  layers are concerned with storing and manipulating data. Handling them
+  properly is an essential skill for programming on the ML-level of Isabelle
+  programming. The most basic layer are theories. They contain global data and
+  can be seen as the ``long-term memory'' of Isabelle. There is usually only
+  one theory active at each moment. Proof contexts and local theories, on the
   other hand, store local data for a task at hand. They act like the
-  ``short-term memory'' and there can be many of them that are active
-  in parallel. 
+  ``short-term memory'' and there can be many of them that are active in
+  parallel.
 *}
 
 section {* Theories\label{sec:theories} (TBD) *}