clarified
authorhaftmann
Fri, 02 Nov 2007 18:52:57 +0100
changeset 25266 37aa898e0523
parent 25265 3a5d33e8a019
child 25267 1f745c599b5c
clarified
doc-src/IsarRef/syntax.tex
--- 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.