1 files changed, 3 insertions, 3 deletions
diff --git a/doc/RefMan-lib.tex b/doc/RefMan-lib.tex
index df4e12c389..89895a8a31 100755
--- a/doc/RefMan-lib.tex
+++ b/doc/RefMan-lib.tex
@@ -76,13 +76,13 @@ extension
 
 \medskip
 
-\noindent Remark: The implication is not defined but primitive
+\Rem The implication is not defined but primitive
 (it is a non-dependent product of a proposition over another proposition).
 There is also a primitive universal quantification (it is a
 dependent product over a proposition). The primitive universal
 quantification allows both first-order and higher-order
-quantification. There is no need to
-use the notation {\tt ( ALL} {\ident} \zeroone{{\tt :} {\specif}} {\tt
+quantification. There is true reason to
+have the notation {\tt ( ALL} {\ident} \zeroone{{\tt :} {\specif}} {\tt
 |} {\form} {\tt )} propositions), except to have a notation dual of
 the notation for first-order existential quantification.
 \caption{Syntax of formulas}