src/Doc/Isar_Ref/Spec.thy

   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}. 
+    \item rewrite morphisms by means of \emph{rewrite definitions}. 
   \end{enumerate}
   
   \begin{matharray}{rcl}
     @{command_def "permanent_interpretation"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
   \end{matharray}

   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
+  (see \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
+  also \emph{rewrite definitions} may be specified.  Semantically, a
+  rewrite definition
+  
+  \begin{itemize}
+  
+    \item produces a corresponding definition in
+      the local theory's underlying target \emph{and}
+    
+    \item augments the rewrite morphism with the equation
+      stemming from the symmetric of the corresponding definition.
+  
+  \end{itemize}
+  
+  This is technically different to to a naive combination
+  of a conventional definition and an explicit rewrite equation:
+  
+  \begin{itemize}
+  
+    \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
+  \end{itemize}
+  
+  Rewrite definitions yield a pattern for introducing new explicit
   operations for existing terms after interpretation.
   
   \end{description}
 \<close>