--- a/ProgTutorial/FirstSteps.thy	Wed Apr 08 13:42:18 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Wed Apr 08 22:47:39 2009 +0100
@@ -57,8 +57,24 @@
   code, rather they indicate what the response is when the code is evaluated.
 
   Once a portion of code is relatively stable, you usually want to export it
-  to a separate ML-file. Such files can then be included in a theory by using
-  the \isacommand{uses}-command in the header of the theory, like:
+  to a separate ML-file. Such files can then be included somewhere inside a 
+  theory by using the command \isacommand{use}. For example
+
+  \begin{center}
+  \begin{tabular}{@ {}l}
+  \isacommand{theory} FirstSteps\\
+  \isacommand{imports} Main\\
+  \isacommand{uses}~@{text "(\"file_to_be_included.ML\")"} @{text "\<dots>"}\\
+  \isacommand{begin}\\
+  \ldots\\
+  \isacommand{use}~@{text "\"file_to_be_included.ML\""}\\
+  \ldots
+  \end{tabular}
+  \end{center}
+
+  The \isacommand{uses}-command in the header of the theory is needed in order 
+  to indicate the dependency of the theory on the ML-file. Alternatively, the 
+  file can be included by just writing in the header
 
   \begin{center}
   \begin{tabular}{@ {}l}
@@ -69,7 +85,8 @@
   \ldots
   \end{tabular}
   \end{center}
-  
+
+  Note that no parentheses are given this time.
 *}
 
 section {* Debugging and Printing\label{sec:printing} *}
@@ -227,6 +244,8 @@
 section {* Combinators\label{sec:combinators} *}
 
 text {*
+  (FIXME: Calling convention)
+
   For beginners perhaps the most puzzling parts in the existing code of Isabelle are
   the combinators. At first they seem to greatly obstruct the
   comprehension of the code, but after getting familiar with them, they
@@ -1554,6 +1573,7 @@
   valid local theory.
 *}
 
+(*
 ML{*signature UNIVERSAL_TYPE =
 sig
   type t
@@ -1616,6 +1636,10 @@
 
 ML_val{*structure Datatab = TableFun(type key = int val ord = int_ord);*}
 
+ML {* LocalTheory.restore *}
+ML {* LocalTheory.set_group *}
+*)
+
 section {* Storing Theorems\label{sec:storing} (TBD) *}
 
 text {* @{ML PureThy.add_thms_dynamic} *}