author nipkow Mon, 06 Dec 1993 09:35:35 +0100 changeset 185 b63888ea0b28 parent 184 236b655114a1 child 186 320f6bdb593a
Typos and style
 doc-src/Ref/theories.tex file | annotate | diff | comparison | revisions
--- a/doc-src/Ref/theories.tex	Fri Dec 03 17:45:19 1993 +0100
+++ b/doc-src/Ref/theories.tex	Mon Dec 06 09:35:35 1993 +0100
@@ -214,7 +214,7 @@

\ttindex{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
+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}
@@ -252,12 +252,14 @@
\begin{ttbox}
orphan = A
\end{ttbox}
-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}.
+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$).
+Creating {\tt orphan.thy} enables automatic loading of $orphan$'s parents.
+If {\tt orphan.ML} depended on no theory then {\tt Pure} should 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
@@ -283,15 +285,15 @@
together with the state if they were declared in the current database.  E.g.
changes made to a reference variable declared in the $Pure$ database are $not$
saved if made while using a child database.  Therefore a new {\tt Readthy}
-structure has to be declared by
+structure has to be created by
\begin{ttbox}
structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
+variable \verb$loaded_thys$ the list of already loaded theories is preserved.
\section{Basic operations on theories}