--- a/ProgTutorial/Advanced.thy	Sat Nov 21 00:29:43 2009 +0100
+++ b/ProgTutorial/Advanced.thy	Sun Nov 22 03:13:29 2009 +0100
@@ -14,18 +14,27 @@
 chapter {* Advanced Isabelle *}
 
 text {*
-  TBD
+  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
+  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. 
 *}
 
 section {* Theories\label{sec:theories} (TBD) *}
 
 text {*
-  Theories are the most fundamental building blocks in Isabelle. They 
-  contain definitions, syntax declarations, axioms, proofs etc. If a definition
-  is stated, it must be stored in a theory in order to be usable later
-  on. Similar with proofs: once a proof is finished, the proved theorem
-  needs to be stored in the theorem database of the theory in order to
-  be usable. All relevant data of a theort can be querried as follows.
+  As said above, theories are the most basic layer in Isabelle. They contain
+  definitions, syntax declarations, axioms, proofs etc. If a definition is
+  stated, it must be stored in a theory in order to be usable later
+  on. Similar with proofs: once a proof is finished, the proved theorem needs
+  to be stored in the theorem database of the theory in order to be
+  usable. All relevant data of a theory can be queried as follows.
 
   \begin{isabelle}
   \isacommand{print\_theory}\\
@@ -43,23 +52,14 @@
   @{text "> theorems: \<dots>"}
   \end{isabelle}
 
+
+
   \begin{center}
   \begin{tikzpicture}
   \node[top color=white, bottom color=gray!30, draw=black!100, drop shadow] {A};
   \end{tikzpicture}
   \end{center}
 
-
-  In contrast to an ordinary theory, which simply consists of a type
-  signature, as well as tables for constants, axioms and theorems, a local
-  theory contains additional context information, such as locally fixed
-  variables and local assumptions that may be used by the package. The type
-  @{ML_type local_theory} is identical to the type of \emph{proof contexts}
-  @{ML_type "Proof.context"}, although not every proof context constitutes a
-  valid local theory.
-
-  @{ML "Context.>> o Context.map_theory"}
-
   \footnote{\bf FIXME: list append in merge operations can cause 
   exponential blowups.}
 *}
@@ -124,6 +124,15 @@
 section {* Local Theories (TBD) *}
 
 text {*
+  In contrast to an ordinary theory, which simply consists of a type
+  signature, as well as tables for constants, axioms and theorems, a local
+  theory contains additional context information, such as locally fixed
+  variables and local assumptions that may be used by the package. The type
+  @{ML_type local_theory} is identical to the type of \emph{proof contexts}
+  @{ML_type "Proof.context"}, although not every proof context constitutes a
+  valid local theory.
+
+  @{ML "Context.>> o Context.map_theory"}
   @{ML_ind "Local_Theory.declaration"}
 *}