diff -r f27a30a18a17 -r 10cf84e5d2c2 doc-src/Logics/intro.tex
--- 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