diff -r 2c8b2fb54b88 -r 16d92d37a8a1 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Fri Nov 14 13:18:33 2014 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy	Fri Nov 14 18:39:42 2014 +0100
@@ -1,5 +1,5 @@
 theory Spec
-imports Base Main
+imports Base Main "~~/src/Tools/Permanent_Interpretation"
 begin
 
 chapter \<open>Specifications\<close>
@@ -796,6 +796,81 @@
 \<close>
 
 
+subsubsection \<open>Permanent locale interpretation\<close>
+
+text \<open>
+  Permanent locale interpretation is a library extension on top
+  of @{command "interpretation"} and @{command "sublocale"}.  It is
+  available by importing theory @{file "~~/src/Tools/Permanent_Interpretation.thy"}
+  and provides
+  \begin{enumerate}
+    \item a unified view on arbitrary suitable local theories as interpretation target; 
+    \item rewrite morphisms by means of \emph{mixin definitions}. 
+  \end{enumerate}
+  
+  \begin{matharray}{rcl}
+    @{command_def "permanent_interpretation"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
+  \end{matharray}
+
+  @{rail \<open>
+    @@{command permanent_interpretation} @{syntax locale_expr} \<newline>
+      definitions? equations?
+    ;
+
+    definitions: @'defining' (@{syntax thmdecl}? @{syntax name} \<newline>
+      @{syntax mixfix}? @'=' @{syntax term} + @'and');
+    equations: @'where' (@{syntax thmdecl}? @{syntax prop} + @'and')
+  \<close>}
+
+  \begin{description}
+
+  \item @{command "permanent_interpretation"}~@{text "expr \<DEFINING> defs \<WHERE> eqns"}
+  interprets @{text expr} in the current local theory.  The command
+  generates proof obligations for the instantiated specifications.
+  Instantiated declarations (in particular, facts) are added to the
+  local theory's underlying target in a post-processing phase.  When
+  adding declarations to locales, interpreted versions of these
+  declarations are added to any target for all interpretations
+  in that target as well. That is, permanent interpretations
+  dynamically participate in any declarations added to
+  locales.
+  
+  The local theory's underlying target must explicitly support
+  permanent interpretations.  Prominent examples are global theories
+  (where @{command "permanent_interpretation"} is technically
+  corresponding to @{command "interpretation"}) and locales
+  (where @{command "permanent_interpretation"} is technically
+  corresponding to @{command "sublocale"}).  Unnamed contexts
+  \secref{sec:target} are not admissible since they are
+  non-permanent due to their very nature.  
+
+  In additions to \emph{rewrite morphisms} specified by @{text eqns},
+  also \emph{mixin definitions} may be specified.  Semantically, a
+  mixin definition results in a corresponding definition in
+  the local theory's underlying target \emph{and} a mixin equation
+  in the resulting rewrite morphisms which is symmetric to the
+  original definition equation.
+  
+  The technical difference to a conventional definition plus
+  an explicit mixin equation is that
+  
+  \begin{enumerate}
+  
+    \item definitions are parsed in the syntactic interpretation
+      context, just like equations;
+  
+    \item the proof needs not consider the equations stemming from
+      definitions -- they are proved implicitly by construction.
+      
+  \end{enumerate}
+  
+  Mixin definitions yield a pattern for introducing new explicit
+  operations for existing terms after interpretation.
+  
+  \end{description}
+\<close>
+
+
 section \<open>Classes \label{sec:class}\<close>
 
 text \<open>