# HG changeset patch
# User wenzelm
# Date 1258924231 -3600
# Node ID 1436dd2bd565764d60862d6f2df76116159913ea
# Parent  cf8365a709119b317891bc75830ac8f743dc9f11# Parent  91f3fc0364cf0dceb1124c354d4978fa8f1c69b1
merged

diff -r 91f3fc0364cf -r 1436dd2bd565 NEWS
--- a/NEWS	Sun Nov 22 22:04:51 2009 +0100
+++ b/NEWS	Sun Nov 22 22:10:31 2009 +0100
@@ -110,31 +110,25 @@
 * ML antiquotation @{code_datatype} inserts definition of a datatype
 generated by the code generator; e.g. see src/HOL/Predicate.thy.
 
-* Combined former theories Divides and IntDiv to one theory Divides in
-the spirit of other number theory theories in HOL; some constants (and
-to a lesser extent also facts) have been suffixed with _nat and _int
-respectively.  INCOMPATIBILITY.
-
 * Most rules produced by inductive and datatype package have mandatory
 prefixes.  INCOMPATIBILITY.
 
 * Reorganization of number theory, INCOMPATIBILITY:
-  - former session NumberTheory now named Old_Number_Theory
-  - new session Number_Theory; prefer this, if possible
-  - moved legacy theories Legacy_GCD and Primes from src/HOL/Library
-    to src/HOL/Old_Number_Theory
+  - new number theory development for nat and int, in
+    theories Divides and GCD as well as in new session
+    Number_Theory
+  - some constants and facts now suffixed with _nat and
+    _int accordingly
+  - former session NumberTheory now named Old_Number_Theory,
+    including theories Legacy_GCD and Primes (prefer Number_Theory
+    if possible)
   - moved theory Pocklington from src/HOL/Library to
     src/HOL/Old_Number_Theory
-  - removed various references to Old_Number_Theory from HOL
-    distribution
 
 * Theory GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm
 of finite and infinite sets. It is shown that they form a complete
 lattice.
 
-* Split off prime number ingredients from theory GCD to theory
-Number_Theory/Primes.
-
 * Class semiring_div requires superclass no_zero_divisors and proof of
 div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
 div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
diff -r 91f3fc0364cf -r 1436dd2bd565 doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Sun Nov 22 22:04:51 2009 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy	Sun Nov 22 22:10:31 2009 +0100
@@ -288,13 +288,62 @@
 section {* Locales \label{sec:locale} *}
 
 text {*
-  Locales are named local contexts, consisting of a list of
+  Locales are parametric named local contexts, consisting of a list of
   declaration elements that are modeled after the Isar proof context
   commands (cf.\ \secref{sec:proof-context}).
 *}
 
 
-subsection {* Locale specifications *}
+subsection {* Locale expressions \label{sec:locale-expr} *}
+
+text {*
+  A \emph{locale expression} denotes a structured context composed of
+  instances of existing locales.  The context consists of a list of
+  instances of declaration elements from the locales.  Two locale
+  instances are equal if they are of the same locale and the
+  parameters are instantiated with equivalent terms.  Declaration
+  elements from equal instances are never repeated, thus avoiding
+  duplicate declarations.
+
+  \indexouternonterm{localeexpr}
+  \begin{rail}
+    localeexpr: (instance + '+') ('for' (fixes + 'and'))?
+    ;
+    instance: (qualifier ':')? nameref (posinsts | namedinsts)
+    ;
+    qualifier: name ('?' | '!')?
+    ;
+    posinsts: (term | '_')*
+    ;
+    namedinsts: 'where' (name '=' term + 'and')
+    ;
+  \end{rail}
+
+  A locale instance consists of a reference to a locale and either
+  positional or named parameter instantiations.  Identical
+  instantiations (that is, those that instante a parameter by itself)
+  may be omitted.  The notation `\_' enables to omit the instantiation
+  for a parameter inside a positional instantiation.
+
+  Terms in instantiations are from the context the locale expressions
+  is declared in.  Local names may be added to this context with the
+  optional for clause.  In addition, syntax declarations from one
+  instance are effective when parsing subsequent instances of the same
+  expression.
+
+  Instances have an optional qualifier which applies to names in
+  declarations.  Names include local definitions and theorem names.
+  If present, the qualifier itself is either optional
+  (``\texttt{?}''), which means that it may be omitted on input of the
+  qualified name, or mandatory (``\texttt{!}'').  If neither
+  ``\texttt{?}'' nor ``\texttt{!}'' are present, the command's default
+  is used.  For @{command "interpretation"} and @{command "interpret"}
+  the default is ``mandatory'', for @{command "locale"} and @{command
+  "sublocale"} the default is ``optional''.
+*}
+
+
+subsection {* Locale declarations *}
 
 text {*
   \begin{matharray}{rcl}
@@ -305,31 +354,22 @@
     @{method_def unfold_locales} & : & @{text method} \\
   \end{matharray}
 
-  \indexouternonterm{contextexpr}\indexouternonterm{contextelem}
+  \indexouternonterm{contextelem}
   \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
   \indexisarelem{defines}\indexisarelem{notes}
   \begin{rail}
-    'locale' name ('=' localeexpr)? 'begin'?
-    ;
-    'print\_locale' '!'? localeexpr
+    'locale' name ('=' locale)? 'begin'?
     ;
-    localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+))
+    'print\_locale' '!'? nameref
     ;
-
-    contextexpr: nameref | '(' contextexpr ')' |
-    (contextexpr (name mixfix? +)) | (contextexpr + '+')
+    locale: contextelem+ | localeexpr ('+' (contextelem+))?
     ;
-    contextelem: fixes | constrains | assumes | defines | notes
-    ;
-    fixes: 'fixes' ((name ('::' type)? structmixfix? | vars) + 'and')
-    ;
-    constrains: 'constrains' (name '::' type + 'and')
-    ;
-    assumes: 'assumes' (thmdecl? props + 'and')
-    ;
-    defines: 'defines' (thmdecl? prop proppat? + 'and')
-    ;
-    notes: 'notes' (thmdef? thmrefs + 'and')
+    contextelem:
+    'fixes' (fixes + 'and')
+    | 'constrains' (name '::' type + 'and')
+    | 'assumes' (props + 'and')
+    | 'defines' (thmdecl? prop proppat? + 'and')
+    | 'notes' (thmdef? thmrefs + 'and')
     ;
   \end{rail}
 
@@ -345,22 +385,17 @@
   care of the most general typing that the combined context elements
   may acquire.
 
-  The @{text import} consists of a structured context expression,
-  consisting of references to existing locales, renamed contexts, or
-  merged contexts.  Renaming uses positional notation: @{text "c
-  x\<^sub>1 \<dots> x\<^sub>n"} means that (a prefix of) the fixed
-  parameters of context @{text c} are named @{text "x\<^sub>1, \<dots>,
-  x\<^sub>n"}; a ``@{text _}'' (underscore) means to skip that
-  position.  Renaming by default deletes concrete syntax, but new
-  syntax may by specified with a mixfix annotation.  An exeption of
-  this rule is the special syntax declared with ``@{text
-  "(\<STRUCTURE>)"}'' (see below), which is neither deleted nor can it
-  be changed.  Merging proceeds from left-to-right, suppressing any
-  duplicates stemming from different paths through the import
-  hierarchy.
+  The @{text import} consists of a structured locale expression; see
+  \secref{sec:proof-context} above.  Its for clause defines the local
+  parameters of the @{text import}.  In addition, locale parameters
+  whose instantance is omitted automatically extend the (possibly
+  empty) for clause: they are inserted at its beginning.  This means
+  that these parameters may be referred to from within the expression
+  and also in the subsequent context elements and provides a
+  notational convenience for the inheritance of parameters in locale
+  declarations.
 
-  The @{text body} consists of basic context elements, further context
-  expressions may be included as well.
+  The @{text body} consists of context elements.
 
   \begin{description}
 
@@ -371,7 +406,9 @@
   implicitly in this context.
 
   \item @{element "constrains"}~@{text "x :: \<tau>"} introduces a type
-  constraint @{text \<tau>} on the local parameter @{text x}.
+  constraint @{text \<tau>} on the local parameter @{text x}.  This
+  element is deprecated.  The type constaint should be introduced in
+  the for clause or the relevant @{element "fixes"} element.
 
   \item @{element "assumes"}~@{text "a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}
   introduces local premises, similar to @{command "assume"} within a
@@ -401,7 +438,7 @@
   \secref{sec:goals}, term bindings may be included as expected,
   though.
   
-  \medskip By default, locale specifications are ``closed up'' by
+  \medskip Locale specifications are ``closed up'' by
   turning the given text into a predicate definition @{text
   loc_axioms} and deriving the original assumptions as local lemmas
   (modulo local definitions).  The predicate statement covers only the
@@ -444,57 +481,72 @@
 *}
 
 
-subsection {* Interpretation of locales *}
+subsection {* Locale interpretations *}
 
 text {*
-  Locale expressions (more precisely, \emph{context expressions}) may
-  be instantiated, and the instantiated facts added to the current
-  context.  This requires a proof of the instantiated specification
-  and is called \emph{locale interpretation}.  Interpretation is
-  possible in theories and locales (command @{command
-  "interpretation"}) and also within a proof body (command @{command
-  "interpret"}).
+  Locale expressions may be instantiated, and the instantiated facts
+  added to the current context.  This requires a proof of the
+  instantiated specification and is called \emph{locale
+  interpretation}.  Interpretation is possible in locales @{command
+  "sublocale"}, theories (command @{command "interpretation"}) and
+  also within a proof body (command @{command "interpret"}).
 
   \begin{matharray}{rcl}
+    @{command_def "sublocale"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
     @{command_def "interpretation"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
-    @{command_def "interpret"} & : & @{text "proof(state) | proof(chain \<rightarrow> proof(prove)"} \\
+    @{command_def "interpret"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
+    @{command_def "print_interps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   \end{matharray}
 
   \indexouternonterm{interp}
   \begin{rail}
-    'interpretation' (interp | name ('<' | subseteq) contextexpr)
+    'sublocale' nameref ('<' | subseteq) localeexpr
     ;
-    'interpret' interp
+    'interpretation' localeepxr equations?
     ;
-    instantiation: ('[' (inst+) ']')?
+    'interpret' localeexpr
     ;
-    interp: (name ':')? \\ (contextexpr instantiation |
-      name instantiation 'where' (thmdecl? prop + 'and'))
+    'print\_interps' nameref
+    ;
+    equations: 'where' (thmdecl? prop + 'and')
     ;
   \end{rail}
 
   \begin{description}
 
-  \item @{command "interpretation"}~@{text "expr insts \<WHERE> eqns"}
+  \item @{command "sublocale"}~@{text "name \<subseteq> expr"}
+  interprets @{text expr} in the locale @{text name}.  A proof that
+  the specification of @{text name} implies the specification of
+  @{text expr} is required.  As in the localized version of the
+  theorem command, the proof is in the context of @{text name}.  After
+  the proof obligation has been dischared, the facts of @{text expr}
+  become part of locale @{text name} as \emph{derived} context
+  elements and are available when the context @{text name} is
+  subsequently entered.  Note that, like import, this is dynamic:
+  facts added to a locale part of @{text expr} after interpretation
+  become also available in @{text name}.
 
-  The first form of @{command "interpretation"} interprets @{text
-  expr} in the theory.  The instantiation is given as a list of terms
-  @{text insts} and is positional.  All parameters must receive an
-  instantiation term --- with the exception of defined parameters.
-  These are, if omitted, derived from the defining equation and other
-  instantiations.  Use ``@{text _}'' to omit an instantiation term.
+  Only specification fragments of @{text expr} that are not already
+  part of @{text name} (be it imported, derived or a derived fragment
+  of the import) are considered in this process.  This enables
+  circular interpretations to the extent that no infinite chains are
+  generated in the locale hierarchy.
 
-  The command generates proof obligations for the instantiated
-  specifications (assumes and defines elements).  Once these are
-  discharged by the user, instantiated facts are added to the theory
-  in a post-processing phase.
+  If interpretations of @{text name} exist in the current theory, the
+  command adds interpretations for @{text expr} as well, with the same
+  qualifier, although only for fragments of @{text expr} that are not
+  interpreted in the theory already.
 
-  Additional equations, which are unfolded in facts during
+  \item @{command "interpretation"}~@{text "expr insts \<WHERE> 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
+  facts are added to the theory in a post-processing phase.
+
+  Additional equations, which are unfolded during
   post-processing, may be given after the keyword @{keyword "where"}.
   This is useful for interpreting concepts introduced through
   definition specification elements.  The equations must be proved.
-  Note that if equations are present, the context expression is
-  restricted to a locale name.
 
   The command is aware of interpretations already active in the
   theory, but does not simplify the goal automatically.  In order to
@@ -506,47 +558,12 @@
   already be active.  The command will only process facts for new
   parts.
 
-  The context expression may be preceded by a name, which takes effect
-  in the post-processing of facts.  It is used to prefix fact names,
-  for example to avoid accidental hiding of other facts.
-
   Adding facts to locales has the effect of adding interpreted facts
   to the theory for all active interpretations also.  That is,
   interpretations dynamically participate in any facts added to
   locales.
 
-  \item @{command "interpretation"}~@{text "name \<subseteq> expr"}
-
-  This form of the command interprets @{text expr} in the locale
-  @{text name}.  It requires a proof that the specification of @{text
-  name} implies the specification of @{text expr}.  As in the
-  localized version of the theorem command, the proof is in the
-  context of @{text name}.  After the proof obligation has been
-  dischared, the facts of @{text expr} become part of locale @{text
-  name} as \emph{derived} context elements and are available when the
-  context @{text name} is subsequently entered.  Note that, like
-  import, this is dynamic: facts added to a locale part of @{text
-  expr} after interpretation become also available in @{text name}.
-  Like facts of renamed context elements, facts obtained by
-  interpretation may be accessed by prefixing with the parameter
-  renaming (where the parameters are separated by ``@{text _}'').
-
-  Unlike interpretation in theories, instantiation is confined to the
-  renaming of parameters, which may be specified as part of the
-  context expression @{text expr}.  Using defined parameters in @{text
-  name} one may achieve an effect similar to instantiation, though.
-
-  Only specification fragments of @{text expr} that are not already
-  part of @{text name} (be it imported, derived or a derived fragment
-  of the import) are considered by interpretation.  This enables
-  circular interpretations.
-
-  If interpretations of @{text name} exist in the current theory, the
-  command adds interpretations for @{text expr} as well, with the same
-  prefix and attributes, although only for fragments of @{text expr}
-  that are not interpreted in the theory already.
-
-  \item @{command "interpret"}~@{text "expr insts \<WHERE> eqns"}
+  \item @{command "interpret"}~@{text "expr insts"}
   interprets @{text expr} in the proof context and is otherwise
   similar to interpretation in theories.
 
@@ -558,7 +575,7 @@
     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
-    issued.
+    added to revert such declarations.
   \end{warn}
 
   \begin{warn}
@@ -566,9 +583,8 @@
     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
-    first.  A warning is issued, since it is likely that these could
-    have been generalized in the first place.  The locale package does
-    not attempt to remove subsumed interpretations.
+    first.  The locale package does not attempt to remove subsumed
+    interpretations.
   \end{warn}
 *}
 
diff -r 91f3fc0364cf -r 1436dd2bd565 doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Sun Nov 22 22:04:51 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Sun Nov 22 22:10:31 2009 +0100
@@ -310,13 +310,63 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Locales are named local contexts, consisting of a list of
+Locales are parametric named local contexts, consisting of a list of
   declaration elements that are modeled after the Isar proof context
   commands (cf.\ \secref{sec:proof-context}).%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Locale specifications%
+\isamarkupsubsection{Locale expressions \label{sec:locale-expr}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+A \emph{locale expression} denotes a structured context composed of
+  instances of existing locales.  The context consists of a list of
+  instances of declaration elements from the locales.  Two locale
+  instances are equal if they are of the same locale and the
+  parameters are instantiated with equivalent terms.  Declaration
+  elements from equal instances are never repeated, thus avoiding
+  duplicate declarations.
+
+  \indexouternonterm{localeexpr}
+  \begin{rail}
+    localeexpr: (instance + '+') ('for' (fixes + 'and'))?
+    ;
+    instance: (qualifier ':')? nameref (posinsts | namedinsts)
+    ;
+    qualifier: name ('?' | '!')?
+    ;
+    posinsts: (term | '_')*
+    ;
+    namedinsts: 'where' (name '=' term + 'and')
+    ;
+  \end{rail}
+
+  A locale instance consists of a reference to a locale and either
+  positional or named parameter instantiations.  Identical
+  instantiations (that is, those that instante a parameter by itself)
+  may be omitted.  The notation `\_' enables to omit the instantiation
+  for a parameter inside a positional instantiation.
+
+  Terms in instantiations are from the context the locale expressions
+  is declared in.  Local names may be added to this context with the
+  optional for clause.  In addition, syntax declarations from one
+  instance are effective when parsing subsequent instances of the same
+  expression.
+
+  Instances have an optional qualifier which applies to names in
+  declarations.  Names include local definitions and theorem names.
+  If present, the qualifier itself is either optional
+  (``\texttt{?}''), which means that it may be omitted on input of the
+  qualified name, or mandatory (``\texttt{!}'').  If neither
+  ``\texttt{?}'' nor ``\texttt{!}'' are present, the command's default
+  is used.  For \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} and \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}
+  the default is ``mandatory'', for \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} and \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}} the default is ``optional''.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Locale declarations%
 }
 \isamarkuptrue%
 %
@@ -329,31 +379,22 @@
     \indexdef{}{method}{unfold\_locales}\hypertarget{method.unfold-locales}{\hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}} & : & \isa{method} \\
   \end{matharray}
 
-  \indexouternonterm{contextexpr}\indexouternonterm{contextelem}
+  \indexouternonterm{contextelem}
   \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
   \indexisarelem{defines}\indexisarelem{notes}
   \begin{rail}
-    'locale' name ('=' localeexpr)? 'begin'?
-    ;
-    'print\_locale' '!'? localeexpr
+    'locale' name ('=' locale)? 'begin'?
     ;
-    localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+))
+    'print\_locale' '!'? nameref
     ;
-
-    contextexpr: nameref | '(' contextexpr ')' |
-    (contextexpr (name mixfix? +)) | (contextexpr + '+')
+    locale: contextelem+ | localeexpr ('+' (contextelem+))?
     ;
-    contextelem: fixes | constrains | assumes | defines | notes
-    ;
-    fixes: 'fixes' ((name ('::' type)? structmixfix? | vars) + 'and')
-    ;
-    constrains: 'constrains' (name '::' type + 'and')
-    ;
-    assumes: 'assumes' (thmdecl? props + 'and')
-    ;
-    defines: 'defines' (thmdecl? prop proppat? + 'and')
-    ;
-    notes: 'notes' (thmdef? thmrefs + 'and')
+    contextelem:
+    'fixes' (fixes + 'and')
+    | 'constrains' (name '::' type + 'and')
+    | 'assumes' (props + 'and')
+    | 'defines' (thmdecl? prop proppat? + 'and')
+    | 'notes' (thmdef? thmrefs + 'and')
     ;
   \end{rail}
 
@@ -369,19 +410,17 @@
   care of the most general typing that the combined context elements
   may acquire.
 
-  The \isa{import} consists of a structured context expression,
-  consisting of references to existing locales, renamed contexts, or
-  merged contexts.  Renaming uses positional notation: \isa{{\isachardoublequote}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isachardoublequote}} means that (a prefix of) the fixed
-  parameters of context \isa{c} are named \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub n{\isachardoublequote}}; a ``\isa{{\isacharunderscore}}'' (underscore) means to skip that
-  position.  Renaming by default deletes concrete syntax, but new
-  syntax may by specified with a mixfix annotation.  An exeption of
-  this rule is the special syntax declared with ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}{\isachardoublequote}}'' (see below), which is neither deleted nor can it
-  be changed.  Merging proceeds from left-to-right, suppressing any
-  duplicates stemming from different paths through the import
-  hierarchy.
+  The \isa{import} consists of a structured locale expression; see
+  \secref{sec:proof-context} above.  Its for clause defines the local
+  parameters of the \isa{import}.  In addition, locale parameters
+  whose instantance is omitted automatically extend the (possibly
+  empty) for clause: they are inserted at its beginning.  This means
+  that these parameters may be referred to from within the expression
+  and also in the subsequent context elements and provides a
+  notational convenience for the inheritance of parameters in locale
+  declarations.
 
-  The \isa{body} consists of basic context elements, further context
-  expressions may be included as well.
+  The \isa{body} consists of context elements.
 
   \begin{description}
 
@@ -391,7 +430,9 @@
   implicitly in this context.
 
   \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}.
+  constraint \isa{{\isasymtau}} on the local parameter \isa{x}.  This
+  element is deprecated.  The type constaint 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}}
   introduces local premises, similar to \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} within a
@@ -421,7 +462,7 @@
   \secref{sec:goals}, term bindings may be included as expected,
   though.
   
-  \medskip By default, locale specifications are ``closed up'' by
+  \medskip Locale specifications are ``closed up'' by
   turning the given text into a predicate definition \isa{loc{\isacharunderscore}axioms} and deriving the original assumptions as local lemmas
   (modulo local definitions).  The predicate statement covers only the
   newly specified assumptions, omitting the content of included locale
@@ -461,56 +502,73 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Interpretation of locales%
+\isamarkupsubsection{Locale interpretations%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Locale expressions (more precisely, \emph{context expressions}) may
-  be instantiated, and the instantiated facts added to the current
-  context.  This requires a proof of the instantiated specification
-  and is called \emph{locale interpretation}.  Interpretation is
-  possible in theories and locales (command \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}) and also within a proof body (command \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}).
+Locale expressions may be instantiated, and the instantiated facts
+  added to the current context.  This requires a proof of the
+  instantiated specification and is called \emph{locale
+  interpretation}.  Interpretation is possible in locales \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}, theories (command \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}) and
+  also within a proof body (command \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}).
 
   \begin{matharray}{rcl}
+    \indexdef{}{command}{sublocale}\hypertarget{command.sublocale}{\hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
     \indexdef{}{command}{interpretation}\hypertarget{command.interpretation}{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
-    \indexdef{}{command}{interpret}\hypertarget{command.interpret}{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isacharbar}\ proof{\isacharparenleft}chain\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
+    \indexdef{}{command}{interpret}\hypertarget{command.interpret}{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isacharbar}\ proof{\isacharparenleft}chain{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
+    \indexdef{}{command}{print\_interps}\hypertarget{command.print-interps}{\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
   \end{matharray}
 
   \indexouternonterm{interp}
   \begin{rail}
-    'interpretation' (interp | name ('<' | subseteq) contextexpr)
+    'sublocale' nameref ('<' | subseteq) localeexpr
     ;
-    'interpret' interp
+    'interpretation' localeepxr equations?
     ;
-    instantiation: ('[' (inst+) ']')?
+    'interpret' localeexpr
     ;
-    interp: (name ':')? \\ (contextexpr instantiation |
-      name instantiation 'where' (thmdecl? prop + 'and'))
+    'print\_interps' nameref
+    ;
+    equations: 'where' (thmdecl? prop + 'and')
     ;
   \end{rail}
 
   \begin{description}
 
-  \item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}
+  \item \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}~\isa{{\isachardoublequote}name\ {\isasymsubseteq}\ expr{\isachardoublequote}}
+  interprets \isa{expr} in the locale \isa{name}.  A proof that
+  the specification of \isa{name} implies the specification of
+  \isa{expr} is required.  As in the localized version of the
+  theorem command, the proof is in the context of \isa{name}.  After
+  the proof obligation has been dischared, the facts of \isa{expr}
+  become part of locale \isa{name} as \emph{derived} context
+  elements and are available when the context \isa{name} is
+  subsequently entered.  Note that, like import, this is dynamic:
+  facts added to a locale part of \isa{expr} after interpretation
+  become also available in \isa{name}.
 
-  The first form of \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} interprets \isa{expr} in the theory.  The instantiation is given as a list of terms
-  \isa{insts} and is positional.  All parameters must receive an
-  instantiation term --- with the exception of defined parameters.
-  These are, if omitted, derived from the defining equation and other
-  instantiations.  Use ``\isa{{\isacharunderscore}}'' to omit an instantiation term.
+  Only specification fragments of \isa{expr} that are not already
+  part of \isa{name} (be it imported, derived or a derived fragment
+  of the import) are considered in this process.  This enables
+  circular interpretations to the extent that no infinite chains are
+  generated in the locale hierarchy.
 
-  The command generates proof obligations for the instantiated
-  specifications (assumes and defines elements).  Once these are
-  discharged by the user, instantiated facts are added to the theory
-  in a post-processing phase.
+  If interpretations of \isa{name} exist in the current theory, the
+  command adds interpretations for \isa{expr} as well, with the same
+  qualifier, although only for fragments of \isa{expr} that are not
+  interpreted in the theory already.
 
-  Additional equations, which are unfolded in facts during
+  \item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}expr\ insts\ {\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
+  facts are added to the theory in a post-processing phase.
+
+  Additional equations, which are unfolded during
   post-processing, may be given after the keyword \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}}.
   This is useful for interpreting concepts introduced through
   definition specification elements.  The equations must be proved.
-  Note that if equations are present, the context expression is
-  restricted to a locale name.
 
   The command is aware of interpretations already active in the
   theory, but does not simplify the goal automatically.  In order to
@@ -522,43 +580,12 @@
   already be active.  The command will only process facts for new
   parts.
 
-  The context expression may be preceded by a name, which takes effect
-  in the post-processing of facts.  It is used to prefix fact names,
-  for example to avoid accidental hiding of other facts.
-
   Adding facts to locales has the effect of adding interpreted facts
   to the theory for all active interpretations also.  That is,
   interpretations dynamically participate in any facts added to
   locales.
 
-  \item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}name\ {\isasymsubseteq}\ expr{\isachardoublequote}}
-
-  This form of the command interprets \isa{expr} in the locale
-  \isa{name}.  It requires a proof that the specification of \isa{name} implies the specification of \isa{expr}.  As in the
-  localized version of the theorem command, the proof is in the
-  context of \isa{name}.  After the proof obligation has been
-  dischared, the facts of \isa{expr} become part of locale \isa{name} as \emph{derived} context elements and are available when the
-  context \isa{name} is subsequently entered.  Note that, like
-  import, this is dynamic: facts added to a locale part of \isa{expr} after interpretation become also available in \isa{name}.
-  Like facts of renamed context elements, facts obtained by
-  interpretation may be accessed by prefixing with the parameter
-  renaming (where the parameters are separated by ``\isa{{\isacharunderscore}}'').
-
-  Unlike interpretation in theories, instantiation is confined to the
-  renaming of parameters, which may be specified as part of the
-  context expression \isa{expr}.  Using defined parameters in \isa{name} one may achieve an effect similar to instantiation, though.
-
-  Only specification fragments of \isa{expr} that are not already
-  part of \isa{name} (be it imported, derived or a derived fragment
-  of the import) are considered by interpretation.  This enables
-  circular interpretations.
-
-  If interpretations of \isa{name} exist in the current theory, the
-  command adds interpretations for \isa{expr} as well, with the same
-  prefix and attributes, although only for fragments of \isa{expr}
-  that are not interpreted in the theory already.
-
-  \item \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}
+  \item \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr\ insts{\isachardoublequote}}
   interprets \isa{expr} in the proof context and is otherwise
   similar to interpretation in theories.
 
@@ -570,7 +597,7 @@
     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
-    issued.
+    added to revert such declarations.
   \end{warn}
 
   \begin{warn}
@@ -578,9 +605,8 @@
     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
-    first.  A warning is issued, since it is likely that these could
-    have been generalized in the first place.  The locale package does
-    not attempt to remove subsumed interpretations.
+    first.  The locale package does not attempt to remove subsumed
+    interpretations.
   \end{warn}%
 \end{isamarkuptext}%
 \isamarkuptrue%