diff --git a/Manual/Description/drules.tex b/Manual/Description/drules.tex
index 4fdb928c61..e6fb3b28de 100644
--- a/Manual/Description/drules.tex
+++ b/Manual/Description/drules.tex
@@ -42,9 +42,9 @@ \section{Simple Derivations}
 
 As an illustration of a proof in \HOL{}, the following chain of
 theorems forms a proof (from the empty set, in the \HOL{} deductive
-system), for the particular terms \ml{``}$t_1$\ml{``}%''
-and \ml{``}$t_2$\ml{``},%''
-both of \HOL\ type \ml{``:bool``}:%''
+system), for the particular terms \ml{``}$t_1$\ml{``}
+and \ml{``}$t_2$\ml{``},
+both of \HOL\ type \ml{``:bool``}:
 
 \begin{enumerate}
 \item $t_1$\ml{ ==> }$t_2$\ml{ |- }$t_1$\ml{ ==> }$t_2$
@@ -94,7 +94,7 @@ \section{Simple Derivations}
 \end{session}
 
 \noindent Each of the three inference steps of the abstract proof
-corresponds to the application%
+corresponds to the application
 %
 \index{inferences, in HOL logic@inferences, in \HOL{} logic!as ML function applications@as \ML\ function applications}%
 \index{proof steps, as ML function applications@proof steps, as \ML\ function applications}%