author lcp Fri Nov 26 16:35:38 1993 +0100 (1993-11-26) changeset 159 3d0324f9417b parent 158 c2fcb6c07689 child 160 80ccb6c354ba
Minor edits to discussion of use_thy
 doc-src/Ref/introduction.tex file | annotate | diff | revisions doc-src/Ref/theories.tex file | annotate | diff | revisions
     1.1 --- a/doc-src/Ref/introduction.tex	Fri Nov 26 13:00:35 1993 +0100
1.2 +++ b/doc-src/Ref/introduction.tex	Fri Nov 26 16:35:38 1993 +0100
1.3 @@ -104,12 +104,12 @@
1.4  reads the given {\it file} as input to the \ML{} session.  Reading a file
1.5  of Isabelle commands is the usual way of replaying a proof.
1.6
1.7 -\item[\ttindexbold{use_thy} \tt"$tname$";]
1.8 -reads a theory definition from file {\it tname}{\tt.thy} and also reads
1.9 -{\ML} commands from the file {\it tname}{\tt.ML}, if it exists.  If theory
1.10 -{\it tname} depends on theories that haven't been read already these are
1.12 -See Chapter~\ref{theories} for details.
1.13 +\item[\ttindexbold{use_thy} \tt"$tname$";]
1.14 +  reads a theory definition from file {\it tname}{\tt.thy} and also reads
1.15 +  {\ML} commands from the file {\it tname}{\tt.ML}, if it exists.  If
1.16 +  theory {\it tname} depends on theories that have not been read already,
1.17 +  then it loads these beforehand.  See Chapter~\ref{theories} for
1.18 +  details.
1.19
1.20  \item[\ttindexbold{time_use} \tt"$file$";]
1.21  performs {\tt use~"$file$"} and prints the total execution time.
1.22 @@ -123,7 +123,7 @@
1.23
1.24  \item[\ttindexbold{loadpath}] contains a list of paths that is used by
1.25  {\tt use_thy} and {\tt update} to find {\it tname}{\tt.ML} and {\it tname}
1.26 -{\tt.thy}. See Chapter~\ref{theories} for details.
1.27 +{\tt.thy}.  See Chapter~\ref{theories} for details.
1.28  \end{description}
1.29
1.30

     2.1 --- a/doc-src/Ref/theories.tex	Fri Nov 26 13:00:35 1993 +0100
2.2 +++ b/doc-src/Ref/theories.tex	Fri Nov 26 16:35:38 1993 +0100
2.3 @@ -181,30 +181,32 @@
2.5  by recursive {\tt use_thy} calls until either an already loaded theory or {\tt
2.6    Pure} is reached.  Therefore one can read a complete logic by just one {\tt
2.7 -use_thy} call if all theories are linked appropriatly.  Afterwards an {\ML}
2.8 +use_thy} call if all theories are linked appropriately.  Afterwards an {\ML}
2.9  structure~$TF$ containing a component {\tt thy} for the new theory and
2.10  components $r@1$ \dots $r@n$ for the rules is declared; it also contains the
2.11  definitions of the {\tt ML} section if any. Unless
2.12  \ttindexbold{delete_tmpfiles} is set to {\tt false}, {\tt.}{\it tf}{\tt.thy.ML}
2.13 -is deleted if no errors occured. Finally the file {\it tf}{\tt.ML} is read, if
2.14 +is deleted if no errors occurred. Finally the file {\it tf}{\tt.ML} is read, if
2.15  it exists; this file normally contains proofs involving the new theory.
2.16
2.17
2.18  \subsection{Filenames and paths}
2.19  \indexbold{filenames}
2.20
2.21 -The files the theory definition resides in must have the lower case name of
2.22 -the theory with ".thy" or ".ML" appended.  On the other hand \ttindex{use_thy}'s
2.23 -parameter has to be the exact theory name.  Optionally the name can be
2.24 -preceeded by a path to specify the directory where the files can be found.  If
2.25 -no path is provided the reference variable \ttindexbold{loadpath} is used which
2.26 -contains a list of paths that are searched in the given order.  After the
2.27 -".thy"-file for a theory has been found, the same path is used to locate the
2.28 -(optional) ".ML"-file.  (You might note that it is also possible to only
2.29 -provide a ".ML"- but no ".thy"-file.  In this case an \ML{} structure with the
2.30 -theory's name has to be created in the ".ML" file.  If both the ".thy"-file
2.31 -and a structure declaration in the ".ML"-file exist the declaration in the
2.32 -latter file is used.  See {\tt ZF/ex/llist.ML} for an example.)
2.33 +The files defining the theory must have the lower case name of the theory
2.34 +with {\tt".thy"} or {\tt".ML"} appended.  On the other hand
2.35 +\ttindex{use_thy}'s parameter has to be the exact theory name.  Optionally
2.36 +the name can be preceded by a path to specify the directory where the
2.37 +files can be found.  If no path is provided the reference variable
2.38 +\ttindexbold{loadpath} is used which contains a list of paths that are
2.39 +searched in the given order.  After the {\tt".thy"}-file for a theory has
2.40 +been found, the same path is used to locate the (optional) {\tt".ML"}-file.
2.41 +
2.42 +It is also possible to provide only a {\tt".ML"}-file, with no
2.43 +{\tt".thy"}-file.  In this case the {\tt".ML"}-file must declare an \ML{}
2.44 +structure having the theory's name.  If both the {\tt".thy"}-file and a
2.45 +structure declaration in the {\tt".ML"}-file exist, then the latter
2.46 +declaration is used.  See {\tt ZF/ex/llist.ML} for an example.
2.47
2.48
2.54 -it (i.e. that have its name in their $theoryDef$) are marked as out-of-date.
2.55 +it (those that have its name in their $theoryDef$) are marked as out-of-date.