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

doc-src/IsarImplementation/Thy/Logic.thy

changeset 29761 | 2b658e50683a |

parent 29758 | 7a3b5bbed313 |

child 29768 | 64a50ff3f308 |

--- a/doc-src/IsarImplementation/Thy/Logic.thy Mon Feb 16 21:23:34 2009 +0100 +++ b/doc-src/IsarImplementation/Thy/Logic.thy Mon Feb 16 21:39:19 2009 +0100 @@ -191,9 +191,9 @@ text {* The language of terms is that of simply-typed @{text "\<lambda>"}-calculus with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72} - or \cite{paulson-ml2}), with the types being determined determined - by the corresponding binders. In contrast, free variables and - constants are have an explicit name and type in each occurrence. + or \cite{paulson-ml2}), with the types being determined by the + corresponding binders. In contrast, free variables and constants + are have an explicit name and type in each occurrence. \medskip A \emph{bound variable} is a natural number @{text "b"}, which accounts for the number of intermediate binders between the