--- a/ProgTutorial/Base.thy	Mon Sep 17 00:07:40 2012 +0100
+++ b/ProgTutorial/Base.thy	Thu Oct 04 13:00:31 2012 +0100
@@ -5,9 +5,6 @@
          "ML_prf" :: prf_decl and
          "ML_val" :: diag
 *)
-uses
-  ("output_tutorial.ML")
-  ("antiquote_setup.ML")
 begin
 
 notation (latex output)
@@ -27,8 +24,8 @@
   HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))
 *}
 
-use "output_tutorial.ML"
-use "antiquote_setup.ML"
+ML_file "output_tutorial.ML"
+ML_file "antiquote_setup.ML"
 
 setup {* OutputTutorial.setup *}
 setup {* AntiquoteSetup.setup *}

--- 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} *}

--- a/ProgTutorial/Package/Simple_Inductive_Package.thy	Mon Sep 17 00:07:40 2012 +0100
+++ b/ProgTutorial/Package/Simple_Inductive_Package.thy	Thu Oct 04 13:00:31 2012 +0100
@@ -1,9 +1,10 @@
 theory Simple_Inductive_Package
 imports Main "../Base"
 keywords "simple_inductive" :: thy_decl
-uses "simple_inductive_package.ML"
 begin
 
+ML_file "simple_inductive_package.ML"
+
 (*
 simple_inductive
   trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"

--- a/ProgTutorial/Recipes/Oracle.thy	Mon Sep 17 00:07:40 2012 +0100
+++ b/ProgTutorial/Recipes/Oracle.thy	Thu Oct 04 13:00:31 2012 +0100
@@ -1,6 +1,5 @@
 theory Oracle
 imports "../Appendix"
-uses ("external_solver.ML")
 begin
 
 section {* Writing an Oracle (TBD)\label{rec:oracle} *} 
@@ -32,7 +31,7 @@
   ``external solver'':
 *}
 
-use "external_solver.ML"
+ML_file "external_solver.ML"
 
 text {*
   We do, however, know that the solver provides a function

Binary file progtutorial.pdf has changed