--- a/doc-src/Ref/introduction.tex Fri Sep 24 12:22:49 1999 +0200
+++ b/doc-src/Ref/introduction.tex Fri Sep 24 12:22:59 1999 +0200
@@ -194,11 +194,11 @@
\item[\ttindexbold{time_use_thy} "$name$";] same as \texttt{use_thy}, but
reports the time taken to process the actual theory parts and {\ML} files
separately.
-
+
\item[\ttindexbold{update_thy} "$name$";] is similar to \texttt{use_thy}, but
ensures that theory $name$ is fully up-to-date with respect to the file
- system --- apart from $name$ itself any of its ancestors may be reloaded as
- well.
+ system --- apart from theory $name$ itself, any of its ancestors may be
+ reloaded as well.
\end{ttdescription}