author | haftmann |
Fri, 02 Nov 2007 18:52:57 +0100 | |
changeset 25266 | 37aa898e0523 |
parent 25265 | 3a5d33e8a019 |
child 25267 | 1f745c599b5c |
--- 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.