summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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. a+x \quad \Var{f}\equiv \lambda x. x+a \quad