doc-src/IsarRef/syntax.tex

   theory & : & \isarantiq \\
   thm & : & \isarantiq \\
   prop & : & \isarantiq \\
   term & : & \isarantiq \\
   const & : & \isarantiq \\
+  abbrev & : & \isarantiq \\
   typeof & : & \isarantiq \\
   typ & : & \isarantiq \\
   thm_style & : & \isarantiq \\
   term_style & : & \isarantiq \\
   text & : & \isarantiq \\

 \texttt{{\at}{\ttlbrace}thm~sym~[no_vars]{\ttrbrace}} would print the
 statement where all schematic variables have been replaced by fixed ones,
 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}
 
 \begin{rail}

     'theory' options name |
     'thm' options thmrefs |
     'prop' options prop |
     'term' options term |
     'const' options term |
+    'abbrev' options term |
     'typeof' options term |
     'typ' options type |
     'thm\_style' options name thmref |
     'term\_style' options name term |
     'text' options name |

 \item [$\at\{prop~\phi\}$] prints a well-typed proposition $\phi$.
 
 \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$.
 
 \item [$\at\{typ~\tau\}$] prints a well-formed type $\tau$.