From d49ab3070e1c58981024a0431db1a32126e9aa9d Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Fri, 28 Jul 2023 16:44:24 +1000 Subject: [PATCH] Fix a variety of documentation typos Closes #1133 --- Manual/Description/misc.tex | 2 +- Manual/Interaction-emacs/interaction-emacs.stex | 6 +++--- Manual/Tutorial/euclid.stex | 8 ++++---- 3 files changed, 8 insertions(+), 8 deletions(-) diff --git a/Manual/Description/misc.tex b/Manual/Description/misc.tex index ea21b639c1..6c19e7541c 100644 --- a/Manual/Description/misc.tex +++ b/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. diff --git a/Manual/Interaction-emacs/interaction-emacs.stex b/Manual/Interaction-emacs/interaction-emacs.stex index fc2f074c74..0874a355fe 100644 --- a/Manual/Interaction-emacs/interaction-emacs.stex +++ b/Manual/Interaction-emacs/interaction-emacs.stex @@ -55,7 +55,7 @@ To install the scripts, add the following lines to your emacs initialisation fil (load "/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 } with the path to your HOL4 installation. /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} diff --git a/Manual/Tutorial/euclid.stex b/Manual/Tutorial/euclid.stex index 5e85cf0a21..0d41f21ebf 100644 --- a/Manual/Tutorial/euclid.stex +++ b/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}