--- a/ProgTutorial/First_Steps.thy	Mon Sep 17 00:07:40 2012 +0100
+++ b/ProgTutorial/First_Steps.thy	Thu Oct 04 13:00:31 2012 +0100
@@ -72,43 +72,21 @@
   However, both commands will only play minor roles in this tutorial (we most of
   the time make sure that the ML-code is defined outside proofs).
 
-  
-
-
+ 
   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 somewhere inside a 
-  theory by using the command \isacommand{use}. For example
+  theory by using the command \isacommand{ML\_file}. For example
 
   \begin{quote}
   \begin{tabular}{@ {}l}
   \isacommand{theory} First\_Steps\\
   \isacommand{imports} Main\\
-  \isacommand{uses}~@{text "(\"file_to_be_included.ML\")"} @{text "\<dots>"}\\
   \isacommand{begin}\\
   \ldots\\
-  \isacommand{use}~@{text "\"file_to_be_included.ML\""}\\
+  \isacommand{ML\_file}~@{text "\"file_to_be_included.ML\""}\\
   \ldots
   \end{tabular}
   \end{quote}
-
-  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{quote}
-  \begin{tabular}{@ {}l}
-  \isacommand{theory} First\_Steps\\
-  \isacommand{imports} Main\\
-  \isacommand{uses} @{text "\"file_to_be_included.ML\""} @{text "\<dots>"}\\
-  \isacommand{begin}\\
-  \ldots
-  \end{tabular}
-  \end{quote}
-
-  Note that no parentheses are given in this case. Note also that the included
-  ML-file should not contain any \isacommand{use} itself. Otherwise Isabelle
-  is unable to record all file dependencies, which is a nuisance if you have
-  to track down errors.
 *}
 
 section {* Printing and Debugging\label{sec:printing} *}