Documentation of 'interpret' updated.

--- a/NEWS	Sat Jul 31 21:14:20 2010 +0200
+++ b/NEWS	Sat Jul 31 23:32:05 2010 +0200
@@ -20,6 +20,15 @@
 files exclusively use the .ML extension.  Minor INCOMPATIBILTY.
 
 
+*** Pure ***
+
+* Interpretation command 'interpret' accepts a list of equations like
+'interpretation' does.
+
+* Diagnostic command 'print_interps' prints interpretations in proofs
+in addition to interpretations in theories.
+
+
 *** HOL ***
 
 * code generator: export_code without explicit file declaration prints

--- a/doc-src/IsarRef/Thy/Spec.thy	Sat Jul 31 21:14:20 2010 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy	Sat Jul 31 23:32:05 2010 +0200
@@ -407,7 +407,7 @@
 
   \item @{element "constrains"}~@{text "x :: \<tau>"} introduces a type
   constraint @{text \<tau>} on the local parameter @{text x}.  This
-  element is deprecated.  The type constaint should be introduced in
+  element is deprecated.  The type constraint should be introduced in
   the for clause or the relevant @{element "fixes"} element.
 
   \item @{element "assumes"}~@{text "a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}
@@ -501,7 +501,7 @@
     ;
     'interpretation' localeepxr equations?
     ;
-    'interpret' localeexpr
+    'interpret' localeexpr equations?
     ;
     'print\_interps' nameref
     ;
@@ -560,14 +560,16 @@
   interpretations dynamically participate in any facts added to
   locales.
 
-  \item @{command "interpret"}~@{text "expr"}
-  interprets @{text expr} in the proof context and is otherwise
-  similar to interpretation in theories.
+  \item @{command "interpret"}~@{text "expr \<WHERE> eqns"} interprets
+  @{text expr} in the proof context and is otherwise similar to
+  interpretation in theories.  Note that rewrite rules given to
+  @{command "interpret"} should be explicitly universally quantified.
 
   \item @{command "print_interps"}~@{text "locale"} lists all
-  interpretations of @{text "locale"} in the current theory, including
-  those due to a combination of an @{command "interpretation"} and
-  one or several @{command "sublocale"} declarations.
+  interpretations of @{text "locale"} in the current theory or proof
+  context, including those due to a combination of a @{command
+  "interpretation"} or @{command "interpret"} and one or several
+  @{command "sublocale"} declarations.
 
   \end{description}
 
@@ -581,7 +583,7 @@
   \end{warn}
 
   \begin{warn}
-    An interpretation in a theory may subsume previous
+    An interpretation in a theory or proof context may subsume previous
     interpretations.  This happens if the same specification fragment
     is interpreted twice and the instantiation of the second
     interpretation is more general than the interpretation of the

--- a/doc-src/IsarRef/Thy/document/Spec.tex	Sat Jul 31 21:14:20 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Sat Jul 31 23:32:05 2010 +0200
@@ -431,7 +431,7 @@
 
   \item \hyperlink{element.constrains}{\mbox{\isa{\isakeyword{constrains}}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isachardoublequote}} introduces a type
   constraint \isa{{\isasymtau}} on the local parameter \isa{x}.  This
-  element is deprecated.  The type constaint should be introduced in
+  element is deprecated.  The type constraint should be introduced in
   the for clause or the relevant \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} element.
 
   \item \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}
@@ -523,7 +523,7 @@
     ;
     'interpretation' localeepxr equations?
     ;
-    'interpret' localeexpr
+    'interpret' localeexpr equations?
     ;
     'print\_interps' nameref
     ;
@@ -582,14 +582,15 @@
   interpretations dynamically participate in any facts added to
   locales.
 
-  \item \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr{\isachardoublequote}}
-  interprets \isa{expr} in the proof context and is otherwise
-  similar to interpretation in theories.
+  \item \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr\ {\isasymWHERE}\ eqns{\isachardoublequote}} interprets
+  \isa{expr} in the proof context and is otherwise similar to
+  interpretation in theories.  Note that rewrite rules given to
+  \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}} should be explicitly universally quantified.
 
   \item \hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}~\isa{{\isachardoublequote}locale{\isachardoublequote}} lists all
-  interpretations of \isa{{\isachardoublequote}locale{\isachardoublequote}} in the current theory, including
-  those due to a combination of an \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} and
-  one or several \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}} declarations.
+  interpretations of \isa{{\isachardoublequote}locale{\isachardoublequote}} in the current theory or proof
+  context, including those due to a combination of a \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} or \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}} and one or several
+  \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}} declarations.
 
   \end{description}
 
@@ -603,7 +604,7 @@
   \end{warn}
 
   \begin{warn}
-    An interpretation in a theory may subsume previous
+    An interpretation in a theory or proof context may subsume previous
     interpretations.  This happens if the same specification fragment
     is interpreted twice and the instantiation of the second
     interpretation is more general than the interpretation of the