diff -r ad4c98fd367b -r 165c97f9bb63 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Wed Aug 24 12:05:48 2005 +0200
+++ b/doc-src/IsarRef/generic.tex	Wed Aug 24 12:07:00 2005 +0200
@@ -260,7 +260,7 @@
   ;
   'interpret' interp
   ;
-  printinterps name
+  printinterps '!'? name
   ;
   interp: thmdecl? contextexpr ('[' (inst+) ']')?
   ;
@@ -314,7 +314,7 @@
   become part of locale $name$ as \emph{derived} context elements and
   are available when the context $name$ is subsequently entered.
   Note that, like import, this is dynamic: facts added to a locale
-  part of $expr$ after the interpretation become also available in
+  part of $expr$ after interpretation become also available in
   $name$.  Like facts
   of renamed context elements, facts obtained by interpretation may be
   accessed by prefixing with the parameter renaming (where the parameters
@@ -330,6 +330,11 @@
   are considered by interpretation.  This enables circular
   interpretations.
 
+  If interpretations of $name$ exist in the current theory, the
+  command adds interpretations for $expr$ as well, with the same
+  prefix and attributes, although only for fragments of $expr$ that
+  are not interpreted in the theory already.
+
 \item [$\isarcmd{interpret}~expr~insts$]
   interprets $expr$ in the proof context and is otherwise similar to
   interpretation in theories.  Free variables in instantiations are not
@@ -337,7 +342,11 @@
 
 \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.
+  active in the current context, either theory or proof context.  The
+  exclamation point argument causes triggers printing of
+  \emph{witness} theorems justifying interpretations.  These are
+  normally omitted from the output.
+
   
 \end{descr}
 
@@ -356,7 +365,7 @@
   in the first place.  The locale package does not attempt to remove
   subsumed interpretations.  This situation is normally harmless, but
   note that $blast$ gets confused by the presence of multiple axclass
-  instances a rule.
+  instances of a rule.
 \end{warn}