diff options
| -rwxr-xr-x | doc/RefMan-pro.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/RefMan-pro.tex b/doc/RefMan-pro.tex index 68f96f7cca..7565612d14 100755 --- a/doc/RefMan-pro.tex +++ b/doc/RefMan-pro.tex @@ -155,8 +155,8 @@ as a {\tt Theorem}, the name {\ident} is known at all section levels: {\tt Defined} (see \ref{Defined}) in order to define a transparent constant. -\item {\tt Local {\ident} : {\form}.} -\comindex{Local} +\item {\tt Let {\ident} : {\form}.} +\comindex{Let} Analogous to {\tt Definition} except that the definition is turned into a local definition on objects depending on it after closing the |