# HG changeset patch
# User lcp
# Date 754328138 -3600
# Node ID 3d0324f9417b0d81995eac57400771aec7352dc4
# Parent  c2fcb6c07689222eca292c0ebb2e3d5a8763fc5f
Minor edits to discussion of use_thy

diff -r c2fcb6c07689 -r 3d0324f9417b doc-src/Ref/introduction.tex
--- a/doc-src/Ref/introduction.tex	Fri Nov 26 13:00:35 1993 +0100
+++ b/doc-src/Ref/introduction.tex	Fri Nov 26 16:35:38 1993 +0100
@@ -104,12 +104,12 @@
 reads the given {\it file} as input to the \ML{} session.  Reading a file
 of Isabelle commands is the usual way of replaying a proof.
 
-\item[\ttindexbold{use_thy} \tt"$tname$";]  
-reads a theory definition from file {\it tname}{\tt.thy} and also reads
-{\ML} commands from the file {\it tname}{\tt.ML}, if it exists.  If theory
-{\it tname} depends on theories that haven't been read already these are
-loaded automatically.
-See Chapter~\ref{theories} for details.
+\item[\ttindexbold{use_thy} \tt"$tname$";] 
+  reads a theory definition from file {\it tname}{\tt.thy} and also reads
+  {\ML} commands from the file {\it tname}{\tt.ML}, if it exists.  If
+  theory {\it tname} depends on theories that have not been read already,
+  then it loads these beforehand.  See Chapter~\ref{theories} for
+  details.
 
 \item[\ttindexbold{time_use} \tt"$file$";]  
 performs {\tt use~"$file$"} and prints the total execution time.
@@ -123,7 +123,7 @@
 
 \item[\ttindexbold{loadpath}] contains a list of paths that is used by 
 {\tt use_thy} and {\tt update} to find {\it tname}{\tt.ML} and {\it tname}
-{\tt.thy}. See Chapter~\ref{theories} for details.
+{\tt.thy}.  See Chapter~\ref{theories} for details.
 \end{description}
 
 
diff -r c2fcb6c07689 -r 3d0324f9417b doc-src/Ref/theories.tex
--- a/doc-src/Ref/theories.tex	Fri Nov 26 13:00:35 1993 +0100
+++ b/doc-src/Ref/theories.tex	Fri Nov 26 16:35:38 1993 +0100
@@ -181,30 +181,32 @@
 loading}  Any of the parent theories that have not been loaded yet are read now
 by recursive {\tt use_thy} calls until either an already loaded theory or {\tt
   Pure} is reached.  Therefore one can read a complete logic by just one {\tt
-use_thy} call if all theories are linked appropriatly.  Afterwards an {\ML}
+use_thy} call if all theories are linked appropriately.  Afterwards an {\ML}
 structure~$TF$ containing a component {\tt thy} for the new theory and
 components $r@1$ \dots $r@n$ for the rules is declared; it also contains the
 definitions of the {\tt ML} section if any. Unless
 \ttindexbold{delete_tmpfiles} is set to {\tt false}, {\tt.}{\it tf}{\tt.thy.ML}
-is deleted if no errors occured. Finally the file {\it tf}{\tt.ML} is read, if
+is deleted if no errors occurred. Finally the file {\it tf}{\tt.ML} is read, if
 it exists; this file normally contains proofs involving the new theory.
 
 
 \subsection{Filenames and paths}
 \indexbold{filenames}
 
-The files the theory definition resides in must have the lower case name of
-the theory with ".thy" or ".ML" appended.  On the other hand \ttindex{use_thy}'s
-parameter has to be the exact theory name.  Optionally the name can be
-preceeded by a path to specify the directory where the files can be found.  If
-no path is provided the reference variable \ttindexbold{loadpath} is used which
-contains a list of paths that are searched in the given order.  After the
-".thy"-file for a theory has been found, the same path is used to locate the
-(optional) ".ML"-file.  (You might note that it is also possible to only
-provide a ".ML"- but no ".thy"-file.  In this case an \ML{} structure with the
-theory's name has to be created in the ".ML" file.  If both the ".thy"-file
-and a structure declaration in the ".ML"-file exist the declaration in the
-latter file is used.  See {\tt ZF/ex/llist.ML} for an example.)
+The files defining the theory must have the lower case name of the theory
+with {\tt".thy"} or {\tt".ML"} appended.  On the other hand
+\ttindex{use_thy}'s parameter has to be the exact theory name.  Optionally
+the name can be preceded by a path to specify the directory where the
+files can be found.  If no path is provided the reference variable
+\ttindexbold{loadpath} is used which contains a list of paths that are
+searched in the given order.  After the {\tt".thy"}-file for a theory has
+been found, the same path is used to locate the (optional) {\tt".ML"}-file.
+
+It is also possible to provide only a {\tt".ML"}-file, with no
+{\tt".thy"}-file.  In this case the {\tt".ML"}-file must declare an \ML{}
+structure having the theory's name.  If both the {\tt".thy"}-file and a
+structure declaration in the {\tt".ML"}-file exist, then the latter
+declaration is used.  See {\tt ZF/ex/llist.ML} for an example.
 
 
 \subsection{Reloading a theory}
@@ -218,7 +220,7 @@
 stops if they are equal. In case the files have been moved, {\tt use_thy}
 searches them the same way a new theory would be searched for.  After all these
 tests have been passed, the theory is reloaded and all theories that depend on
-it (i.e. that have its name in their $theoryDef$) are marked as out-of-date.
+it (those that have its name in their $theoryDef$) are marked as out-of-date.
 
 As changing a theory often makes it necessary to reload all theories that
 (indirectly) depend on it, \ttindexbold{update} should be used instead of {\tt