1.1 --- a/Admin/E/README	Mon Nov 23 19:42:52 2009 +0100
     1.2 +++ b/Admin/E/README	Mon Nov 23 21:56:07 2009 +0100
     1.3 @@ -1,4 +1,3 @@
     1.4 -
     1.5  This distribution of E 1.0-004 has been compiled according to the
     1.6  README included in the official version from
     1.7  http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html
     1.8 @@ -8,23 +7,12 @@
     1.9    $ ./configure
    1.10    $ make
    1.11  
    1.12 -The resulting PROVER/eproof executable has been changed to be
    1.13 -relocatable:
    1.14 -
    1.15 -  $ diff eproof-orig eproof
    1.16 -  1c1
    1.17 -  < #!/bin/bash -f
    1.18 -  ---
    1.19 -  > #!/usr/bin/env bash
    1.20 -  3c3,4
    1.21 -  < EXECPATH=/Users/schulz/SOURCES/Projects/E/PROVER
    1.22 -  ---
    1.23 -  > set -o noglob
    1.24 -  > EXECPATH="$(cd "$(dirname "$0")"; pwd)"
    1.25 +The PROVER/eproof executable has been replaced by a version written in
    1.26 +perl (by Sascha Boehme).
    1.27  
    1.28  Now the main executables in PROVER/ are moved to the platform-specific
    1.29  target directory (E/x86-linux etc.).
    1.30  
    1.31  
    1.32 -	Makarius
    1.33 -	07-Apr-2009
    1.34 +        Makarius
    1.35 +        23-Nov-2009

     2.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Mon Nov 23 19:42:52 2009 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Mon Nov 23 21:56:07 2009 +0100
     2.3 @@ -456,13 +456,10 @@
     2.4    \secref{sec:object-logic}).  Separate introduction rules @{text
     2.5    loc_axioms.intro} and @{text loc.intro} are provided as well.
     2.6    
     2.7 -  \item @{command "print_locale"}~@{text "import + body"} prints the
     2.8 -  specified locale expression in a flattened form.  The notable
     2.9 -  special case @{command "print_locale"}~@{text loc} just prints the
    2.10 -  contents of the named locale, but keep in mind that type-inference
    2.11 -  will normalize type variables according to the usual alphabetical
    2.12 -  order.  The command omits @{element "notes"} elements by default.
    2.13 -  Use @{command "print_locale"}@{text "!"} to get them included.
    2.14 +  \item @{command "print_locale"}~@{text "locale"} prints the
    2.15 +  contents of the named locale.  The command omits @{element "notes"}
    2.16 +  elements by default.  Use @{command "print_locale"}@{text "!"} to
    2.17 +  have them included.
    2.18  
    2.19    \item @{command "print_locales"} prints the names of all locales
    2.20    of the current theory.
    2.21 @@ -537,7 +534,7 @@
    2.22    qualifier, although only for fragments of @{text expr} that are not
    2.23    interpreted in the theory already.
    2.24  
    2.25 -  \item @{command "interpretation"}~@{text "expr insts \<WHERE> eqns"}
    2.26 +  \item @{command "interpretation"}~@{text "expr \<WHERE> eqns"}
    2.27    interprets @{text expr} in the theory.  The command generates proof
    2.28    obligations for the instantiated specifications (assumes and defines
    2.29    elements).  Once these are discharged by the user, instantiated
    2.30 @@ -563,19 +560,24 @@
    2.31    interpretations dynamically participate in any facts added to
    2.32    locales.
    2.33  
    2.34 -  \item @{command "interpret"}~@{text "expr insts"}
    2.35 +  \item @{command "interpret"}~@{text "expr"}
    2.36    interprets @{text expr} in the proof context and is otherwise
    2.37    similar to interpretation in theories.
    2.38  
    2.39 +  \item @{command "print_interps"}~@{text "locale"} lists all
    2.40 +  interpretations of @{text "locale"} in the current theory, including
    2.41 +  those due to a combination of an @{command "interpretation"} and
    2.42 +  one or several @{command "sublocale"} declarations.
    2.43 +
    2.44    \end{description}
    2.45  
    2.46    \begin{warn}
    2.47      Since attributes are applied to interpreted theorems,
    2.48      interpretation may modify the context of common proof tools, e.g.\
    2.49 -    the Simplifier or Classical Reasoner.  Since the behavior of such
    2.50 -    automated reasoning tools is \emph{not} stable under
    2.51 -    interpretation morphisms, manual declarations might have to be
    2.52 -    added to revert such declarations.
    2.53 +    the Simplifier or Classical Reasoner.  As the behavior of such
    2.54 +    tools is \emph{not} stable under interpretation morphisms, manual
    2.55 +    declarations might have to be added to the target context of the
    2.56 +    interpretation to revert such declarations.
    2.57    \end{warn}
    2.58  
    2.59    \begin{warn}

     3.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Mon Nov 23 19:42:52 2009 +0100
     3.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Mon Nov 23 21:56:07 2009 +0100
     3.3 @@ -478,13 +478,10 @@
     3.4    \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} by \isa{{\isachardoublequote}{\isasymlongrightarrow}{\isachardoublequote}} in HOL; see also
     3.5    \secref{sec:object-logic}).  Separate introduction rules \isa{loc{\isacharunderscore}axioms{\isachardot}intro} and \isa{loc{\isachardot}intro} are provided as well.
     3.6    
     3.7 -  \item \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{{\isachardoublequote}import\ {\isacharplus}\ body{\isachardoublequote}} prints the
     3.8 -  specified locale expression in a flattened form.  The notable
     3.9 -  special case \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{loc} just prints the
    3.10 -  contents of the named locale, but keep in mind that type-inference
    3.11 -  will normalize type variables according to the usual alphabetical
    3.12 -  order.  The command omits \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}} elements by default.
    3.13 -  Use \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to get them included.
    3.14 +  \item \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{{\isachardoublequote}locale{\isachardoublequote}} prints the
    3.15 +  contents of the named locale.  The command omits \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}}
    3.16 +  elements by default.  Use \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to
    3.17 +  have them included.
    3.18  
    3.19    \item \hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}} prints the names of all locales
    3.20    of the current theory.
    3.21 @@ -559,7 +556,7 @@
    3.22    qualifier, although only for fragments of \isa{expr} that are not
    3.23    interpreted in the theory already.
    3.24  
    3.25 -  \item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}
    3.26 +  \item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}expr\ {\isasymWHERE}\ eqns{\isachardoublequote}}
    3.27    interprets \isa{expr} in the theory.  The command generates proof
    3.28    obligations for the instantiated specifications (assumes and defines
    3.29    elements).  Once these are discharged by the user, instantiated
    3.30 @@ -585,19 +582,24 @@
    3.31    interpretations dynamically participate in any facts added to
    3.32    locales.
    3.33  
    3.34 -  \item \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr\ insts{\isachardoublequote}}
    3.35 +  \item \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr{\isachardoublequote}}
    3.36    interprets \isa{expr} in the proof context and is otherwise
    3.37    similar to interpretation in theories.
    3.38  
    3.39 +  \item \hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}~\isa{{\isachardoublequote}locale{\isachardoublequote}} lists all
    3.40 +  interpretations of \isa{{\isachardoublequote}locale{\isachardoublequote}} in the current theory, including
    3.41 +  those due to a combination of an \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} and
    3.42 +  one or several \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}} declarations.
    3.43 +
    3.44    \end{description}
    3.45  
    3.46    \begin{warn}
    3.47      Since attributes are applied to interpreted theorems,
    3.48      interpretation may modify the context of common proof tools, e.g.\
    3.49 -    the Simplifier or Classical Reasoner.  Since the behavior of such
    3.50 -    automated reasoning tools is \emph{not} stable under
    3.51 -    interpretation morphisms, manual declarations might have to be
    3.52 -    added to revert such declarations.
    3.53 +    the Simplifier or Classical Reasoner.  As the behavior of such
    3.54 +    tools is \emph{not} stable under interpretation morphisms, manual
    3.55 +    declarations might have to be added to the target context of the
    3.56 +    interpretation to revert such declarations.
    3.57    \end{warn}
    3.58  
    3.59    \begin{warn}

     4.1 --- a/doc-src/Locales/Locales/Examples3.thy	Mon Nov 23 19:42:52 2009 +0100
     4.2 +++ b/doc-src/Locales/Locales/Examples3.thy	Mon Nov 23 21:56:07 2009 +0100
     4.3 @@ -591,7 +591,7 @@
     4.4    ( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\
     4.5    \textit{instance} & ::=
     4.6    & [ \textit{qualifier} ``\textbf{:}'' ]
     4.7 -    \textit{qualified-name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
     4.8 +    \textit{name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
     4.9    \textit{expression}  & ::= 
    4.10    & \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$
    4.11      [ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex]
    4.12 @@ -625,8 +625,8 @@
    4.13  
    4.14    \textit{toplevel} & ::=
    4.15    & \textbf{print\_locales} \\
    4.16 -  & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{locale} \\
    4.17 -  & | & \textbf{print\_interps} \textit{locale}
    4.18 +  & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{name} \\
    4.19 +  & | & \textbf{print\_interps} \textit{name}
    4.20  \end{tabular}
    4.21  \end{center}
    4.22  \hrule

     5.1 --- a/doc-src/Locales/Locales/document/Examples3.tex	Mon Nov 23 19:42:52 2009 +0100
     5.2 +++ b/doc-src/Locales/Locales/document/Examples3.tex	Mon Nov 23 21:56:07 2009 +0100
     5.3 @@ -882,7 +882,7 @@
     5.4    ( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\
     5.5    \textit{instance} & ::=
     5.6    & [ \textit{qualifier} ``\textbf{:}'' ]
     5.7 -    \textit{qualified-name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
     5.8 +    \textit{name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
     5.9    \textit{expression}  & ::= 
    5.10    & \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$
    5.11      [ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex]
    5.12 @@ -916,8 +916,8 @@
    5.13  
    5.14    \textit{toplevel} & ::=
    5.15    & \textbf{print\_locales} \\
    5.16 -  & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{locale} \\
    5.17 -  & | & \textbf{print\_interps} \textit{locale}
    5.18 +  & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{name} \\
    5.19 +  & | & \textbf{print\_interps} \textit{name}
    5.20  \end{tabular}
    5.21  \end{center}
    5.22  \hrule