--- a/doc-src/Ref/theories.tex Thu Nov 25 14:23:04 1993 +0100
+++ b/doc-src/Ref/theories.tex Thu Nov 25 14:32:54 1993 +0100
@@ -173,25 +173,21 @@
\label{LoadingTheories}
\subsection{Reading a new theory}
-\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
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
-{\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}
+{\tt.}{\it tf}{\tt.thy.ML}, and reads the latter file. \indexbold{automatic
+loading} 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. 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.
+\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}