diff -r 1e93eb09ebb9 -r f27a30a18a17 doc-src/Intro/foundations.tex
--- a/doc-src/Intro/foundations.tex	Wed Jul 02 11:59:10 1997 +0200
+++ b/doc-src/Intro/foundations.tex	Wed Jul 02 16:46:36 1997 +0200
@@ -79,7 +79,7 @@
 Note that there are two versions of function application syntax
 available in Isabelle: either $t\,u$, which is the usual form for
 higher-order languages, or $t(u)$, trying to look more like
-first-order. The latter syntax is used throughout the manual.
+first-order.  The latter syntax is used throughout the manual.
 \[ 
 \index{lambda abs@$\lambda$-abstractions}\index{function applications}
 \begin{array}{ll}
@@ -602,7 +602,7 @@
 
   \item Even an equation such as $\Var{f}(a)\qeq a+a$ is all right.  It has
 four solutions, but Isabelle evaluates them lazily, trying projection before
-imitation. The first solution is usually the one desired:
+imitation.  The first solution is usually the one desired:
 \[ \Var{f}\equiv \lambda x. x+x \quad
    \Var{f}\equiv \lambda x. a+x \quad
    \Var{f}\equiv \lambda x. x+a \quad