diff -r 9c19f90272e8 -r 8fcacb0e3b15 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Fri Dec 08 23:25:54 2006 +0100
+++ b/doc-src/IsarRef/generic.tex	Sat Dec 09 18:05:34 2006 +0100
@@ -6,13 +6,14 @@
 
 \indexisarcmd{axiomatization}
 \indexisarcmd{definition}\indexisaratt{defn}
-\indexisarcmd{abbreviation}
+\indexisarcmd{abbreviation}\indexisarcmd{print-abbrevs}
 \indexisarcmd{notation}
 \begin{matharray}{rcll}
   \isarcmd{axiomatization} & : & \isarkeep{local{\dsh}theory} & (axiomatic!)\\
   \isarcmd{definition} & : & \isarkeep{local{\dsh}theory} \\
   defn & : & \isaratt \\
   \isarcmd{abbreviation} & : & \isarkeep{local{\dsh}theory} \\
+  \isarcmd{print_abbrevs}^* & : & \isarkeep{theory~|~proof} \\
   \isarcmd{notation} & : & \isarkeep{local{\dsh}theory} \\
 \end{matharray}
 
@@ -82,6 +83,9 @@
   that affects the concrete syntax declared for abbreviations, cf.\ 
   $\isarkeyword{syntax}$ in \S\ref{sec:syn-trans}.
   
+\item $\isarkeyword{print_abbrevs}$ prints all constant abbreviations
+  of the current context.
+  
 \item $\isarkeyword{notation}~c~mx$ associates mixfix syntax with an
   existing constant or fixed variable.  This is a robust interface to
   the underlying $\isarkeyword{syntax}$ primitive