--- 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}