duplicate words removed

HOL-Theorem-Prover · Aug 14, 2014 · 2a2de91 · 2a2de91
1 parent 192323e
commit 2a2de91
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git a/Manual/Description/definitions.tex b/Manual/Description/definitions.tex
@@ -309,7 +309,7 @@ \subsection{Type definitions that fail}
 \end{verbatim}
 \end{hol}
 %
-Recursion on the left must fail for for cardinality reasons. For
+Recursion on the left must fail for cardinality reasons. For
 example, HOL does not allow the following attempt to model the untyped
 lambda calculus as a set (note the \holtxt{->} in the clause for the
 \holtxt{Abs} constructor):

diff --git a/Manual/Description/libraries.tex b/Manual/Description/libraries.tex
@@ -1457,7 +1457,7 @@ \subsection{Support for high-level proof steps}
   apart to find a term and a measure function with which to induct.
   For example, if one wanted to induct on the length of a list
   \holtxt{L}, the invocation \ml{measureInduct\_on~`LENGTH L`}
-  would be be appropriate.
+  would be appropriate.
 
 \item [\ml{recInduct}] takes a induction theorem generated by
 \ml{Define} or \ml{Hol\_defn} and applies it to the current goal.

diff --git a/Manual/Description/theories.tex b/Manual/Description/theories.tex
@@ -4286,7 +4286,7 @@ \subsection{Relations (\theoryimp{relation})}\label{relation}
 %
 Notice that {\small\verb+RTC_RULES+}, in keeping with the definition
 of {\small\verb+RTC+}, extends an \verb+R+-step from \verb+x+ to
-\verb+y+ with a a sequence of \verb+R+-steps from \verb+y+ to \verb+z+
+\verb+y+ with a sequence of \verb+R+-steps from \verb+y+ to \verb+z+
 to construct \verb+RTC x z+. The theorem
 {\small\verb+RTC_RULES_RIGHT1+} first makes a sequence of \verb+R+
 steps and then a single \verb+R+ step to form \verb+RTC x z+. Similar