Fix a variety of documentation typos

Closes #1133

Manual/Description/misc.tex

@@ -72,7 +72,7 @@ \section{The Trace System}
 \index{traces, controlling HOL feedback@traces, controlling \HOL{} feedback}
 \label{sec:traces}
 
-The trace system gives the user one central interface with which to control most of \HOL's many different flags, though they be scattered all over the system, and defined in different modules.
+The trace system gives the user one central interface with which to control most of \HOL's many different flags, though they are scattered all over the system, and defined in different modules.
 These flags are typically those that determine the level to which \HOL{} tools provide information to the user while operating.
 For example, a trace level of zero will usually make a tool remain completely
 silent while it operates.

Manual/Interaction-emacs/interaction-emacs.stex

@@ -55,7 +55,7 @@ To install the scripts, add the following lines to your emacs initialisation fil
 (load "<path>/HOL/tools/hol-unicode")
 \end{code}
 
-If your version of emacs does not highlight the active region be default,
+If your version of emacs does not highlight the active region by default,
 also add the following line to your initialisation file:
 \begin{code}
 (transient-mark-mode 1)
@@ -66,7 +66,7 @@ Restart emacs to make these changes take effect.
 
 \begin{enum}
 \item Start emacs.
-\item Press {\tt C-x C-f} to open a file with file with a name ending in {\tt Script.sml}
+\item Press {\tt C-x C-f} to open a file (its name should have suffix {\tt Script.sml})
 \item Press {\tt M-h H}, then press {\tt RET} or down arrow and then {\tt RET}.
 \end{enum}
 The HOL window should look something like this:
@@ -398,7 +398,7 @@ Replace {\tt <path>} with the path to your HOL4 installation.
 <path>/HOL/help/HOLindex.html
 \end{code}
 
-Once theories has been opened (see Section~\ref{copy}), one can search for theorems in the current
+Once theories have been opened (see Section~\ref{copy}), one can search for theorems in the current
 context using {\tt print\_match}. For example, with {\tt arithmeticTheory} opened, doing {\tt M-h~M-r}
 with the following selected,
 \begin{code}

Manual/Tutorial/euclid.stex

@@ -1108,10 +1108,10 @@ Compiling euclidTheory.sml
 \end{verbatim}
 \end{session}
 
-Now we have created four new files, various forms of \ml{euclidTheory}
-with four different suffixes.  Only \ml{euclidTheory.sig} is really
-suitable for human consumption.  While still in the \ml{euclid}
-directory that we created, we can demonstrate:
+Now we have created four new files: various forms of \ml{euclidTheory}
+with four different suffixes (three of which are hidden in the \texttt{.holobjs} directory).
+Only \ml{euclidTheory.sig} is really suitable for human consumption, and this is put into the same directory as the \texttt{euclidScript.sml} file.
+While still in the \ml{euclid} directory that we created, we can demonstrate:
 
 \begin{session}
 \begin{alltt}