doc-src/Intro/foundations.tex
 changeset 3485 f27a30a18a17 parent 3106 5396e99c02af child 6170 9a59cf8ae9b5
--- 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. x+a \quad