| changeset 25266 | 37aa898e0523 |
| parent 24033 | 386f025be266 |
| child 25521 | 6cebd2ff3ab7 |
--- a/doc-src/IsarRef/syntax.tex Fri Nov 02 16:38:37 2007 +0100 +++ b/doc-src/IsarRef/syntax.tex Fri Nov 02 18:52:57 2007 +0100 @@ -526,7 +526,7 @@ \item [$\at\{term~t\}$] prints a well-typed term $t$. -\item [$\at\{const~c\}$] prints a well-defined constant $c$. +\item [$\at\{const~c\}$] prints a logical or syntactic constant $c$. \item [$\at\{abbrev~c\,\vec x\}$] prints a constant abbreviation $c\,\vec x \equiv rhs$ as defined in the current context.