Generated files.
1.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex Mon Nov 23 21:03:49 2009 +0100
1.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Mon Nov 23 21:04:00 2009 +0100
1.3 @@ -478,13 +478,10 @@
1.4 \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} by \isa{{\isachardoublequote}{\isasymlongrightarrow}{\isachardoublequote}} in HOL; see also
1.5 \secref{sec:object-logic}). Separate introduction rules \isa{loc{\isacharunderscore}axioms{\isachardot}intro} and \isa{loc{\isachardot}intro} are provided as well.
1.6
1.7 - \item \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{{\isachardoublequote}import\ {\isacharplus}\ body{\isachardoublequote}} prints the
1.8 - specified locale expression in a flattened form. The notable
1.9 - special case \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{loc} just prints the
1.10 - contents of the named locale, but keep in mind that type-inference
1.11 - will normalize type variables according to the usual alphabetical
1.12 - order. The command omits \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}} elements by default.
1.13 - Use \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to get them included.
1.14 + \item \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{{\isachardoublequote}locale{\isachardoublequote}} prints the
1.15 + contents of the named locale. The command omits \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}}
1.16 + elements by default. Use \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to
1.17 + have them included.
1.18
1.19 \item \hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}} prints the names of all locales
1.20 of the current theory.
1.21 @@ -559,7 +556,7 @@
1.22 qualifier, although only for fragments of \isa{expr} that are not
1.23 interpreted in the theory already.
1.24
1.25 - \item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}
1.26 + \item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}expr\ {\isasymWHERE}\ eqns{\isachardoublequote}}
1.27 interprets \isa{expr} in the theory. The command generates proof
1.28 obligations for the instantiated specifications (assumes and defines
1.29 elements). Once these are discharged by the user, instantiated
1.30 @@ -585,19 +582,24 @@
1.31 interpretations dynamically participate in any facts added to
1.32 locales.
1.33
1.34 - \item \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr\ insts{\isachardoublequote}}
1.35 + \item \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr{\isachardoublequote}}
1.36 interprets \isa{expr} in the proof context and is otherwise
1.37 similar to interpretation in theories.
1.38
1.39 + \item \hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}~\isa{{\isachardoublequote}locale{\isachardoublequote}} lists all
1.40 + interpretations of \isa{{\isachardoublequote}locale{\isachardoublequote}} in the current theory, including
1.41 + those due to a combination of an \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} and
1.42 + one or several \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}} declarations.
1.43 +
1.44 \end{description}
1.45
1.46 \begin{warn}
1.47 Since attributes are applied to interpreted theorems,
1.48 interpretation may modify the context of common proof tools, e.g.\
1.49 - the Simplifier or Classical Reasoner. Since the behavior of such
1.50 - automated reasoning tools is \emph{not} stable under
1.51 - interpretation morphisms, manual declarations might have to be
1.52 - added to revert such declarations.
1.53 + the Simplifier or Classical Reasoner. As the behavior of such
1.54 + tools is \emph{not} stable under interpretation morphisms, manual
1.55 + declarations might have to be added to the target context of the
1.56 + interpretation to revert such declarations.
1.57 \end{warn}
1.58
1.59 \begin{warn}
2.1 --- a/doc-src/Locales/Locales/document/Examples3.tex Mon Nov 23 21:03:49 2009 +0100
2.2 +++ b/doc-src/Locales/Locales/document/Examples3.tex Mon Nov 23 21:04:00 2009 +0100
2.3 @@ -882,7 +882,7 @@
2.4 ( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\
2.5 \textit{instance} & ::=
2.6 & [ \textit{qualifier} ``\textbf{:}'' ]
2.7 - \textit{qualified-name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
2.8 + \textit{name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
2.9 \textit{expression} & ::=
2.10 & \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$
2.11 [ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex]
2.12 @@ -916,8 +916,8 @@
2.13
2.14 \textit{toplevel} & ::=
2.15 & \textbf{print\_locales} \\
2.16 - & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{locale} \\
2.17 - & | & \textbf{print\_interps} \textit{locale}
2.18 + & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{name} \\
2.19 + & | & \textbf{print\_interps} \textit{name}
2.20 \end{tabular}
2.21 \end{center}
2.22 \hrule