--- a/doc-src/IsarRef/generic.tex Mon Feb 27 12:14:36 2006 +0100
+++ b/doc-src/IsarRef/generic.tex Mon Feb 27 12:20:21 2006 +0100
@@ -430,7 +430,7 @@
\item [$\isarcmd{print_interps}~loc$]
prints the interpretations of a particular locale $loc$ that are
active in the current context, either theory or proof context. The
- exclamation point argument causes triggers printing of
+ exclamation point argument triggers printing of
\emph{witness} theorems justifying interpretations. These are
normally omitted from the output.