author lcp Fri, 26 Nov 1993 16:35:38 +0100 changeset 159 3d0324f9417b parent 158 c2fcb6c07689 child 160 80ccb6c354ba
Minor edits to discussion of use_thy
 doc-src/Ref/introduction.tex file | annotate | diff | comparison | revisions doc-src/Ref/theories.tex file | annotate | diff | comparison | revisions
--- 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$";]
-{\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
-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}


--- 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 @@
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.

-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.
(indirectly) depend on it, \ttindexbold{update} should be used instead of {\tt