doc-src/Locales/Locales/Examples.thy

   current theory; \isakeyword{print\_locale}~$n$ prints the parameters
   and assumptions of locale $n$; \isakeyword{print\_locale!}~$n$
   additionally outputs the conclusions.
 
   The syntax of the locale commands discussed in this tutorial is
-  shown in Table~\ref{tab:commands}.  See the
+  shown in Table~\ref{tab:commands}.  The grammer is complete with the
+  exception of additional context elements not discussed here.  See the
   Isabelle/Isar Reference Manual~\cite{IsarRef}
   for full documentation.  *}
 
 
 section {* Import \label{sec:import} *}