# HG changeset patch # User ballarin # Date 1280611925 -7200 # Node ID 2c1913d1b945713b1c3d04bc10b3e1fd4ef123b9 # Parent 06fd1914b90219fcc93d32321426828909e12f5f Documentation of 'interpret' updated. diff -r 06fd1914b902 -r 2c1913d1b945 NEWS --- 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 diff -r 06fd1914b902 -r 2c1913d1b945 doc-src/IsarRef/Thy/Spec.thy --- 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 :: \"} introduces a type constraint @{text \} 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: \\<^sub>1 \ \\<^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 \ 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 diff -r 06fd1914b902 -r 2c1913d1b945 doc-src/IsarRef/Thy/document/Spec.tex --- 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