diff -r 8fcacb0e3b15 -r 410ca6910f6f doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Sat Dec 09 18:05:34 2006 +0100
+++ b/doc-src/IsarRef/syntax.tex	Sat Dec 09 18:05:36 2006 +0100
@@ -435,6 +435,7 @@
   prop & : & \isarantiq \\
   term & : & \isarantiq \\
   const & : & \isarantiq \\
+  abbrev & : & \isarantiq \\
   typeof & : & \isarantiq \\
   typ & : & \isarantiq \\
   thm_style & : & \isarantiq \\
@@ -465,7 +466,7 @@
 which are easier to read.
 
 \indexisarant{theory}\indexisarant{thm}\indexisarant{prop}\indexisarant{term}\indexisarant{const}
-\indexisarant{typeof}\indexisarant{typ}\indexisarant{thm-style}
+\indexisarant{abbrev}\indexisarant{typeof}\indexisarant{typ}\indexisarant{thm-style}
 \indexisarant{term-style}\indexisarant{text}\indexisarant{goals}
 \indexisarant{subgoals}\indexisarant{prf}\indexisarant{full-prf}\indexisarant{ML}
 \indexisarant{ML-type}\indexisarant{ML-struct}
@@ -480,6 +481,7 @@
     'prop' options prop |
     'term' options term |
     'const' options term |
+    'abbrev' options term |
     'typeof' options term |
     'typ' options type |
     'thm\_style' options name thmref |
@@ -517,6 +519,9 @@
 \item [$\at\{term~t\}$] prints a well-typed term $t$.
 
 \item [$\at\{const~c\}$] prints a well-defined constant $c$.
+  
+\item [$\at\{abbrev~c\,\vec x\}$] prints a constant abbreviation
+  $c\,\vec x \equiv rhs$ as defined in the current context.
 
 \item [$\at\{typeof~t\}$] prints the type of a well-typed term $t$.