# HG changeset patch
# User wenzelm
# Date 1265113356 -3600
# Node ID fd90fb0903c019b972d5a47eca7192efdd7c4a78
# Parent  f3bce1cc513ca3bb52ff992c1abed2de67cb2f22
minimal tuning of this slightly dated material;

diff -r f3bce1cc513c -r fd90fb0903c0 doc-src/IsarImplementation/Thy/Integration.thy
--- a/doc-src/IsarImplementation/Thy/Integration.thy	Tue Feb 02 13:11:04 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Integration.thy	Tue Feb 02 13:22:36 2010 +0100
@@ -79,8 +79,9 @@
   \item @{ML Toplevel.is_toplevel}~@{text "state"} checks for an empty
   toplevel state.
 
-  \item @{ML Toplevel.theory_of}~@{text "state"} selects the theory of
-  a theory or proof (!), otherwise raises @{ML Toplevel.UNDEF}.
+  \item @{ML Toplevel.theory_of}~@{text "state"} selects the
+  background theory of @{text "state"}, raises @{ML Toplevel.UNDEF}
+  for an empty toplevel state.
 
   \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof
   state if available, otherwise raises @{ML Toplevel.UNDEF}.
@@ -114,16 +115,16 @@
   The operational part is represented as the sequential union of a
   list of partial functions, which are tried in turn until the first
   one succeeds.  This acts like an outer case-expression for various
-  alternative state transitions.  For example, \isakeyword{qed} acts
+  alternative state transitions.  For example, \isakeyword{qed} works
   differently for a local proofs vs.\ the global ending of the main
   proof.
 
   Toplevel transitions are composed via transition transformers.
   Internally, Isar commands are put together from an empty transition
-  extended by name and source position (and optional source text).  It
-  is then left to the individual command parser to turn the given
-  concrete syntax into a suitable transition transformer that adjoins
-  actual operations on a theory or proof state etc.
+  extended by name and source position.  It is then left to the
+  individual command parser to turn the given concrete syntax into a
+  suitable transition transformer that adjoins actual operations on a
+  theory or proof state etc.
 *}
 
 text %mlref {*
@@ -188,7 +189,7 @@
   the toplevel itself, and only make sense in interactive mode.  Under
   normal circumstances, the user encounters these only implicitly as
   part of the protocol between the Isabelle/Isar system and a
-  user-interface such as ProofGeneral.
+  user-interface such as Proof~General.
 
   \begin{description}
 
@@ -323,9 +324,7 @@
   associated with each theory, by declaring these dependencies in the
   theory header as @{text \<USES>}, and loading them consecutively
   within the theory context.  The system keeps track of incoming {\ML}
-  sources and associates them with the current theory.  The file
-  @{text A}\verb,.ML, is loaded after a theory has been concluded, in
-  order to support legacy proof {\ML} proof scripts.
+  sources and associates them with the current theory.
 
   The basic internal actions of the theory database are @{text
   "update"}, @{text "outdate"}, and @{text "remove"}:
@@ -386,12 +385,15 @@
 
   \item @{ML use_thy}~@{text A} ensures that theory @{text A} is fully
   up-to-date wrt.\ the external file store, reloading outdated
-  ancestors as required.
+  ancestors as required.  In batch mode, the simultaneous @{ML
+  use_thys} should be used exclusively.
 
   \item @{ML use_thys} is similar to @{ML 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.
+  result.  By loading a whole sub-graph of theories like that, the
+  intrinsic parallelism can be exploited by the system, to speedup
+  loading.
 
   \item @{ML ThyInfo.touch_thy}~@{text A} performs and @{text outdate} action
   on theory @{text A} and all descendants.