# HG changeset patch
# User nipkow
# Date 753989206 -3600
# Node ID 4f83c0a0c3f4682852853484074824200259f9e8
# Parent  9ba8bff1addca05c25b863320318b1be2f11dc70
minor changes

diff -r 9ba8bff1addc -r 4f83c0a0c3f4 doc-src/Ref/theories.tex
--- a/doc-src/Ref/theories.tex	Mon Nov 22 16:03:36 1993 +0100
+++ b/doc-src/Ref/theories.tex	Mon Nov 22 18:26:46 1993 +0100
@@ -79,17 +79,15 @@
 The different parts of a theory definition are interpreted as follows:
 \begin{description} 
 \item[$theoryDef$] A theory has a name $id$ and is an
-  extension of the union of theories $id@1$ \dots $id@n$ with new
+  extension of the union of theories $name@1$ \dots $name@n$ with new
   classes, types, constants, syntax and axioms. The basic theory, which 
   contains only the meta-logic, is called {\tt Pure}.
 
-  If $name@i$ is a string the theory $name@i$ is {\em not} used in building
-  the base of theory $id$.  The reason for using strings in $theoryDef$ is that
-  many theories use objects created in a \ML-file that does not belong to a
-  theory itself.  Because $name@1$ \dots $name@n$ are loaded automatically a
-  string can be used to specify a file that is needed as a series of 
-  \ML{}-declarations but not as a parent for theory $id$.  See
-  Chapter~\ref{LoadingTheories} for details.
+  If $name@i$ is a string, then theory $name@i$ is {\em not} used in building
+  the base of theory $id$. Strings stand for ML-files rather than
+  theory-files and document the dependence if $id$ on additional files. This
+  is required because $name@1$ \dots $name@n$ are loaded automatically when
+  theory $id$ is (re)built. See Chapter~\ref{LoadingTheories} for details.
 \item[$class$] The new class $id$ is declared as a subclass of existing
   classes $id@1$ \dots $id@n$.  This rules out cyclic class structures.
   Isabelle automatically computes the transitive closure of subclass
@@ -140,23 +138,22 @@
 \begin{ttbox} 
 use_thy: string -> unit
 \end{ttbox}
-
 Each theory definition must reside in a separate file.  Let the file {\it
-tf}{\tt.thy} contain the definition of a theory called $TF$ with parent
+  tf}{\tt.thy} contain the definition of a theory called $TF$ with parent
 theories $TB@1$ \dots $TB@n$.  Calling \ttindexbold{use_thy}~{\tt"}{\it
-TF\/}{\tt"} reads file {\it tf}{\tt.thy}, writes an intermediate {\ML}-file
+  TF\/}{\tt"} reads file {\it tf}{\tt.thy}, writes an intermediate {\ML}-file
 {\tt.}{\it tf}{\tt.thy.ML}, and reads the latter file.  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} 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. (Normally {\tt.}{\it tf}{\tt.thy.ML} is deleted now if
-there have occured no errors. In case one wants to have a look at it,
-{\tt delete_tmpfiles := false} can be set before calling {\tt use_thy}.)  
-Finally the file {\it tf}{\tt.ML} is read, if it exists; this file normally
-contains proofs involving the new theory.
+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}
+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 it exists; this file normally contains proofs
+involving the new theory.
 
 
 \subsection{Filenames and paths}
@@ -167,9 +164,9 @@
 preceeded by a path to specify the directory where the files can be found.  If
 no path is provided the reference variable {\tt 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
+".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 a \ML{} structure with the
+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.)
@@ -178,15 +175,15 @@
 \subsection{Reloading a theory}
 
 {\tt use_thy} keeps track of all loaded theories and stores information about
-their files.  If it finds that the theory to be loaded was already read before
-the following happens:  First the theory's files are searched at the place
-they were located at the last time they were read. If they are found their
-time of last modification is compared to the internal data and {\tt use_thy}
-stops if they are equal. In case the files have been moved, {\tt use_thy}
-searches them the same way as 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.
+their files.  If it finds that the theory to be loaded was already read
+before, the following happens: First the theory's files are searched at the
+place they were located the last time they were read. If they are found,
+their time of last modification is compared to the internal data and {\tt
+  use_thy} 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.
 
 As changing a theory often makes it necessary to reload all theories that
 (indirectly) depend on it, {\tt update} should be used instead of {\tt
@@ -208,24 +205,25 @@
 \end{center}
 
 Therefore there is a way to link theories and the $orphaned$ \ML-files. The
-link from a theory to a \ML-file has been mentioned in
+link from a theory to an \ML-file has been mentioned in
 Chapter~\ref{DefiningTheories} (strings in $theoryDef$).  But to make this
 work and to establish a link in the opposite direction we need to create a
-{\it pseudo theory}.  Let's assume we have a \ML-file named {\tt orphan.ML} that
-depends on theory $A$ and itself is used in theory $B$.  To link the three we
-have to create the file {\tt orphan.thy} containing the line
+{\it pseudo theory}.  Let's assume we have an \ML-file named {\tt orphan.ML}
+that depends on theory $A$ and is itself used in theory $B$.  To link the
+three we have to create the file {\tt orphan.thy} containing the line
 \begin{ttbox}
 orphan = A
 \end{ttbox}
-and add {\tt "orphan"} to theory $B$'s $theoryDef$.  Creating {\tt orphan.thy}
-is necessary because of two reasons: First it enables automatic loading of
-$orphan$'s parents and second it creates the \ML{}-object {\tt orphan} that
-is needed by {\tt use_thy} (though it is not added to the base of theory $B$). 
-If {\tt orphan.ML} depended on no theory then {\tt Pure} would have been used
-instead of {\tt A}.
+and add {\tt "orphan"} to the list of $B$'s parents.  Creating {\tt
+  orphan.thy} is necessary because of two reasons: First it enables automatic
+loading of $orphan$'s parents and second it creates the \ML{}-object {\tt
+  orphan} that is needed by {\tt use_thy} (though it is not added to the base
+of theory $B$).  If {\tt orphan.ML} depended on no theory then {\tt Pure}
+would have been used instead of {\tt A}.
 
 For an extensive example of how this technique can be used to link over 30
-files and read them by just two {\tt use_thy} calls have a look at the ZF logic.
+files and read them by just two {\tt use_thy} calls have a look at the ZF
+logic.
 
 
 \subsection{Removing a theory}
@@ -252,9 +250,9 @@
 in every newly created database.  This is not necessary if the database is
 created by copying an existent one.
 
-The above declarations are contained in the $Pure$ database, so one could
-simply use e.g. {\tt use_thy} if saving of the reference variables is not
-needed.  Also Standard ML of New Jersey does not have this behaviour.
+%The above declarations are contained in the $Pure$ database, so one could
+%simply use e.g. {\tt use_thy} if saving of the reference variables is not
+%needed.  Standard ML of New Jersey does not have this behaviour.
 
 
 \section{Basic operations on theories}