Now there are TWO spaces after each full stop, so that the Emacs sentence
primitives work

--- a/doc-src/Logics/ZF.tex	Wed Jul 02 16:46:36 1997 +0200
+++ b/doc-src/Logics/ZF.tex	Wed Jul 02 16:53:14 1997 +0200
@@ -808,7 +808,7 @@
 Nested patterns are translated recursively:
 {\tt\%<$x$,$y$,$z$>.$t$} $\leadsto$ {\tt\%<$x$,<$y$,$z$>>.$t$} $\leadsto$
 {\tt split(\%$x$.\%<$y$,$z$>.$t$)} $\leadsto$ {\tt split(\%$x$.split(\%$y$
-  $z$.$t$))}. The reverse translation is performed upon printing.
+  $z$.$t$))}.  The reverse translation is performed upon printing.
 \begin{warn}
   The translation between patterns and {\tt split} is performed automatically
   by the parser and printer.  Thus the internal and external form of a term
@@ -818,7 +818,7 @@
 \end{warn}
 In addition to explicit $\lambda$-abstractions, patterns can be used in any
 variable binding construct which is internally described by a
-$\lambda$-abstraction. Some important examples are
+$\lambda$-abstraction.  Some important examples are
 \begin{description}
 \item[Let:] {\tt let {\it pattern} = $t$ in $u$}
 \item[Choice:] {\tt THE~{\it pattern}~.~$P$}

--- a/doc-src/Logics/intro.tex	Wed Jul 02 16:46:36 1997 +0200
+++ b/doc-src/Logics/intro.tex	Wed Jul 02 16:53:14 1997 +0200
@@ -42,7 +42,7 @@
 \item[\thydx{Cube}] is Barendregt's $\lambda$-cube.
 \end{ttdescription}
 The logics {\tt CCL}, {\tt LCF}, {\tt HOLCF}, {\tt Modal} and {\tt
-  Cube} are currently undocumented. All object-logics' sources are
+  Cube} are currently undocumented.  All object-logics' sources are
 distributed with Isabelle (see the directory \texttt{src}).  They are
 also available for browsing on the WWW at:
 \begin{ttbox}
@@ -135,15 +135,15 @@
 \]
 
 Proof procedures use safe rules whenever possible, delaying the application
-of unsafe rules. Those safe rules are preferred that generate the fewest
-subgoals. Safe rules are (by definition) deterministic, while the unsafe
-rules require search. The design of a suitable set of rules can be as
+of unsafe rules.  Those safe rules are preferred that generate the fewest
+subgoals.  Safe rules are (by definition) deterministic, while the unsafe
+rules require search.  The design of a suitable set of rules can be as
 important as the strategy for applying them.
 
 Many of the proof procedures use backtracking.  Typically they attempt to
 solve subgoal~$i$ by repeatedly applying a certain tactic to it.  This
 tactic, which is known as a {\bf step tactic}, resolves a selection of
-rules with subgoal~$i$. This may replace one subgoal by many;  the
+rules with subgoal~$i$.  This may replace one subgoal by many;  the
 search persists until there are fewer subgoals in total than at the start.
 Backtracking happens when the search reaches a dead end: when the step
 tactic fails.  Alternative outcomes are then searched by a depth-first or