# HG changeset patch
# User wenzelm
# Date 1186678831 -7200
# Node ID c315d0a40db66e69573697911470d9bf494de377
# Parent  92c646714237868920f983cc05b1d5e9db3daa1b
updated;

diff -r 92c646714237 -r c315d0a40db6 doc-src/IsarImplementation/Thy/document/integration.tex
--- a/doc-src/IsarImplementation/Thy/document/integration.tex	Thu Aug 09 16:56:17 2007 +0200
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex	Thu Aug 09 19:00:31 2007 +0200
@@ -442,7 +442,7 @@
 \begin{mldecls}
   \indexml{theory}\verb|theory: string -> theory| \\
   \indexml{use-thy}\verb|use_thy: string -> unit| \\
-  \indexml{update-thy}\verb|update_thy: string -> unit| \\
+  \indexml{use-thys}\verb|use_thys: string list -> unit| \\
   \indexml{touch-thy}\verb|touch_thy: string -> unit| \\
   \indexml{remove-thy}\verb|remove_thy: string -> unit| \\[1ex]
   \indexml{ThyInfo.begin-theory}\verb|ThyInfo.begin_theory|\verb|: ... -> bool -> theory| \\
@@ -458,13 +458,14 @@
   associated with name \isa{A}.  Note that the result might be
   outdated.
 
-  \item \verb|use_thy|~\isa{A} loads theory \isa{A} if it is absent
-  or out-of-date.  It ensures that all parent theories are available
-  as well, but does not reload them if older versions are already
-  present.
+  \item \verb|use_thy|~\isa{A} ensures that theory \isa{A} is fully
+  up-to-date wrt.\ the external file store, reloading outdated
+  ancestors as required.
 
-  \item \verb|update_thy| is similar to \verb|use_thy|, but ensures that
-  theory \isa{A} and all ancestors are fully up-to-date.
+  \item \verb|use_thys| is similar to \verb|use_thy|, but handles
+  several theories simultaneously.  Thus it acts like processing the
+  import header of a theory, without performing the merge of the
+  result, though.
 
   \item \verb|touch_thy|~\isa{A} performs and \isa{outdate} action
   on theory \isa{A} and all descendants.
@@ -473,10 +474,7 @@
   descendants from the theory database.
 
   \item \verb|ThyInfo.begin_theory| is the basic operation behind a
-  \isa{{\isasymTHEORY}} header declaration.  The boolean argument
-  indicates the strictness of treating ancestors: for \verb|true| (as
-  in interactive mode) like \verb|update_thy|, and for \verb|false| (as
-  in batch mode) like \verb|use_thy|.  This is {\ML} functions is
+  \isa{{\isasymTHEORY}} header declaration.  This is {\ML} functions is
   normally not invoked directly.
 
   \item \verb|ThyInfo.end_theory| concludes the loading of a theory