# HG changeset patch # User bulwahn # Date 1259009767 -3600 # Node ID caab5399bb2dd5bb86e4a909c225b37e05568c6f # Parent 5b0d23d2c08f1a5a2fe315b11252feed88966926# Parent 0ec11efb9124b70d59f12f818d14e562b3a4c63d merged diff -r 5b0d23d2c08f -r caab5399bb2d Admin/E/README --- a/Admin/E/README Mon Nov 23 19:42:52 2009 +0100 +++ b/Admin/E/README Mon Nov 23 21:56:07 2009 +0100 @@ -1,4 +1,3 @@ - This distribution of E 1.0-004 has been compiled according to the README included in the official version from http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html @@ -8,23 +7,12 @@ $ ./configure $ make -The resulting PROVER/eproof executable has been changed to be -relocatable: - - $ diff eproof-orig eproof - 1c1 - < #!/bin/bash -f - --- - > #!/usr/bin/env bash - 3c3,4 - < EXECPATH=/Users/schulz/SOURCES/Projects/E/PROVER - --- - > set -o noglob - > EXECPATH="$(cd "$(dirname "$0")"; pwd)" +The PROVER/eproof executable has been replaced by a version written in +perl (by Sascha Boehme). Now the main executables in PROVER/ are moved to the platform-specific target directory (E/x86-linux etc.). - Makarius - 07-Apr-2009 + Makarius + 23-Nov-2009 diff -r 5b0d23d2c08f -r caab5399bb2d doc-src/IsarRef/Thy/Spec.thy --- a/doc-src/IsarRef/Thy/Spec.thy Mon Nov 23 19:42:52 2009 +0100 +++ b/doc-src/IsarRef/Thy/Spec.thy Mon Nov 23 21:56:07 2009 +0100 @@ -456,13 +456,10 @@ \secref{sec:object-logic}). Separate introduction rules @{text loc_axioms.intro} and @{text loc.intro} are provided as well. - \item @{command "print_locale"}~@{text "import + body"} prints the - specified locale expression in a flattened form. The notable - special case @{command "print_locale"}~@{text 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 @{element "notes"} elements by default. - Use @{command "print_locale"}@{text "!"} to get them included. + \item @{command "print_locale"}~@{text "locale"} prints the + contents of the named locale. The command omits @{element "notes"} + elements by default. Use @{command "print_locale"}@{text "!"} to + have them included. \item @{command "print_locales"} prints the names of all locales of the current theory. @@ -537,7 +534,7 @@ qualifier, although only for fragments of @{text expr} that are not interpreted in the theory already. - \item @{command "interpretation"}~@{text "expr insts \ eqns"} + \item @{command "interpretation"}~@{text "expr \ eqns"} interprets @{text 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 @@ -563,19 +560,24 @@ interpretations dynamically participate in any facts added to locales. - \item @{command "interpret"}~@{text "expr insts"} + \item @{command "interpret"}~@{text "expr"} interprets @{text expr} in the proof context and is otherwise similar to interpretation in theories. + \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. + \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 5b0d23d2c08f -r caab5399bb2d doc-src/IsarRef/Thy/document/Spec.tex --- a/doc-src/IsarRef/Thy/document/Spec.tex Mon Nov 23 19:42:52 2009 +0100 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Mon Nov 23 21:56:07 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 5b0d23d2c08f -r caab5399bb2d doc-src/Locales/Locales/Examples3.thy --- a/doc-src/Locales/Locales/Examples3.thy Mon Nov 23 19:42:52 2009 +0100 +++ b/doc-src/Locales/Locales/Examples3.thy Mon Nov 23 21:56:07 2009 +0100 @@ -591,7 +591,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] @@ -625,8 +625,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 diff -r 5b0d23d2c08f -r caab5399bb2d doc-src/Locales/Locales/document/Examples3.tex --- a/doc-src/Locales/Locales/document/Examples3.tex Mon Nov 23 19:42:52 2009 +0100 +++ b/doc-src/Locales/Locales/document/Examples3.tex Mon Nov 23 21:56:07 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