# HG changeset patch
# User wenzelm
# Date 938168579 -7200
# Node ID c29a222cf9814d24af95b521fe854d0c8aa1b64f
# Parent  2d89d12f31eb58f17f653dfc97a554b6c360b0b8
tuned;

diff -r 2d89d12f31eb -r c29a222cf981 doc-src/Ref/introduction.tex
--- 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}