# HG changeset patch
# User ballarin
# Date 1259006640 -3600
# Node ID 62251d6b00386c9cbc1b6327618ab2a38434b345
# Parent  52643d0f856dbd7cd49135b472275663cf9eb9d6
Generated files.

diff -r 52643d0f856d -r 62251d6b0038 doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Mon Nov 23 21:03:49 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Mon Nov 23 21:04:00 2009 +0100
@@ -478,13 +478,10 @@
   \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} by \isa{{\isachardoublequote}{\isasymlongrightarrow}{\isachardoublequote}} in HOL; see also
   \secref{sec:object-logic}).  Separate introduction rules \isa{loc{\isacharunderscore}axioms{\isachardot}intro} and \isa{loc{\isachardot}intro} are provided as well.
   
-  \item \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{{\isachardoublequote}import\ {\isacharplus}\ body{\isachardoublequote}} prints the
-  specified locale expression in a flattened form.  The notable
-  special case \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{loc} just prints the
-  contents of the named locale, but keep in mind that type-inference
-  will normalize type variables according to the usual alphabetical
-  order.  The command omits \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}} elements by default.
-  Use \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to get them included.
+  \item \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{{\isachardoublequote}locale{\isachardoublequote}} prints the
+  contents of the named locale.  The command omits \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}}
+  elements by default.  Use \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to
+  have them included.
 
   \item \hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}} prints the names of all locales
   of the current theory.
@@ -559,7 +556,7 @@
   qualifier, although only for fragments of \isa{expr} that are not
   interpreted in the theory already.
 
-  \item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}
+  \item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}expr\ {\isasymWHERE}\ eqns{\isachardoublequote}}
   interprets \isa{expr} in the theory.  The command generates proof
   obligations for the instantiated specifications (assumes and defines
   elements).  Once these are discharged by the user, instantiated
@@ -585,19 +582,24 @@
   interpretations dynamically participate in any facts added to
   locales.
 
-  \item \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr\ insts{\isachardoublequote}}
+  \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.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.
+
   \end{description}
 
   \begin{warn}
     Since attributes are applied to interpreted theorems,
     interpretation may modify the context of common proof tools, e.g.\
-    the Simplifier or Classical Reasoner.  Since the behavior of such
-    automated reasoning tools is \emph{not} stable under
-    interpretation morphisms, manual declarations might have to be
-    added to revert such declarations.
+    the Simplifier or Classical Reasoner.  As the behavior of such
+    tools is \emph{not} stable under interpretation morphisms, manual
+    declarations might have to be added to the target context of the
+    interpretation to revert such declarations.
   \end{warn}
 
   \begin{warn}
diff -r 52643d0f856d -r 62251d6b0038 doc-src/Locales/Locales/document/Examples3.tex
--- a/doc-src/Locales/Locales/document/Examples3.tex	Mon Nov 23 21:03:49 2009 +0100
+++ b/doc-src/Locales/Locales/document/Examples3.tex	Mon Nov 23 21:04:00 2009 +0100
@@ -882,7 +882,7 @@
   ( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\
   \textit{instance} & ::=
   & [ \textit{qualifier} ``\textbf{:}'' ]
-    \textit{qualified-name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
+    \textit{name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
   \textit{expression}  & ::= 
   & \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$
     [ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex]
@@ -916,8 +916,8 @@
 
   \textit{toplevel} & ::=
   & \textbf{print\_locales} \\
-  & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{locale} \\
-  & | & \textbf{print\_interps} \textit{locale}
+  & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{name} \\
+  & | & \textbf{print\_interps} \textit{name}
 \end{tabular}
 \end{center}
 \hrule