Minor edits to discussion of use_thy
authorlcp
Fri Nov 26 16:35:38 1993 +0100 (1993-11-26)
changeset 1593d0324f9417b
parent 158 c2fcb6c07689
child 160 80ccb6c354ba
Minor edits to discussion of use_thy
doc-src/Ref/introduction.tex
doc-src/Ref/theories.tex
     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.11 -loaded automatically.
    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.4  loading}  Any of the parent theories that have not been loaded yet are read now
     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.49  \subsection{Reloading a theory}
    2.50 @@ -218,7 +220,7 @@
    2.51  stops if they are equal. In case the files have been moved, {\tt use_thy}
    2.52  searches them the same way a new theory would be searched for.  After all these
    2.53  tests have been passed, the theory is reloaded and all theories that depend on
    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.
    2.56  
    2.57  As changing a theory often makes it necessary to reload all theories that
    2.58  (indirectly) depend on it, \ttindexbold{update} should be used instead of {\tt