tuned;
authorwenzelm
Fri Sep 24 12:22:59 1999 +0200 (1999-09-24 ago)
changeset 7592c29a222cf981
parent 7591 2d89d12f31eb
child 7593 6bc8fa8b4b24
tuned;
doc-src/Ref/introduction.tex
     1.1 --- a/doc-src/Ref/introduction.tex	Fri Sep 24 12:22:49 1999 +0200
     1.2 +++ b/doc-src/Ref/introduction.tex	Fri Sep 24 12:22:59 1999 +0200
     1.3 @@ -194,11 +194,11 @@
     1.4  \item[\ttindexbold{time_use_thy} "$name$";] same as \texttt{use_thy}, but
     1.5    reports the time taken to process the actual theory parts and {\ML} files
     1.6    separately.
     1.7 -
     1.8 +  
     1.9  \item[\ttindexbold{update_thy} "$name$";] is similar to \texttt{use_thy}, but
    1.10    ensures that theory $name$ is fully up-to-date with respect to the file
    1.11 -  system --- apart from $name$ itself any of its ancestors may be reloaded as
    1.12 -  well.
    1.13 +  system --- apart from theory $name$ itself, any of its ancestors may be
    1.14 +  reloaded as well.
    1.15    
    1.16  \end{ttdescription}
    1.17