# HG changeset patch
# User haftmann
# Date 1243338049 -7200
# Node ID 0f8cb37bcafd297f090ad2b3fb4c896cdc077c41
# Parent  03a35fbc9dc6f523d17e23724fa51764c8b3cfa9
clarified benefit of interpretation

diff -r 03a35fbc9dc6 -r 0f8cb37bcafd doc-src/Classes/Thy/Classes.thy
--- a/doc-src/Classes/Thy/Classes.thy	Tue May 26 12:31:01 2009 +0200
+++ b/doc-src/Classes/Thy/Classes.thy	Tue May 26 13:40:49 2009 +0200
@@ -485,14 +485,23 @@
   qed
 qed intro_locales
 
+text {*
+  \noindent This pattern is also helpful to reuse abstract
+  specifications on the \emph{same} type.  For example, think of a
+  class @{text preorder}; for type @{typ nat}, there are at least two
+  possible instances: the natural order or the order induced by the
+  divides relation.  But only one of these instances can be used for
+  @{command instantiation}; using the locale behind the class @{text
+  preorder}, it is still possible to utilise the same abstract
+  specification again using @{command interpretation}.
+*}
 
 subsection {* Additional subclass relations *}
 
 text {*
-  Any @{text "group"} is also a @{text "monoid"};  this
-  can be made explicit by claiming an additional
-  subclass relation,
-  together with a proof of the logical difference:
+  Any @{text "group"} is also a @{text "monoid"}; this can be made
+  explicit by claiming an additional subclass relation, together with
+  a proof of the logical difference:
 *}
 
 subclass %quote (in group) monoid
@@ -559,7 +568,7 @@
 subsection {* A note on syntax *}
 
 text {*
-  As a commodity, class context syntax allows to refer
+  As a convenience, class context syntax allows to refer
   to local class operations and their global counterparts
   uniformly;  type inference resolves ambiguities.  For example:
 *}
diff -r 03a35fbc9dc6 -r 0f8cb37bcafd doc-src/Classes/Thy/document/Classes.tex
--- a/doc-src/Classes/Thy/document/Classes.tex	Tue May 26 12:31:01 2009 +0200
+++ b/doc-src/Classes/Thy/document/Classes.tex	Tue May 26 13:40:49 2009 +0200
@@ -922,15 +922,25 @@
 %
 \endisadelimquote
 %
+\begin{isamarkuptext}%
+\noindent This pattern is also helpful to reuse abstract
+  specifications on the \emph{same} type.  For example, think of a
+  class \isa{preorder}; for type \isa{nat}, there are at least two
+  possible instances: the natural order or the order induced by the
+  divides relation.  But only one of these instances can be used for
+  \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}; using the locale behind the class \isa{preorder}, it is still possible to utilise the same abstract
+  specification again using \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isamarkupsubsection{Additional subclass relations%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Any \isa{group} is also a \isa{monoid};  this
-  can be made explicit by claiming an additional
-  subclass relation,
-  together with a proof of the logical difference:%
+Any \isa{group} is also a \isa{monoid}; this can be made
+  explicit by claiming an additional subclass relation, together with
+  a proof of the logical difference:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -1038,7 +1048,7 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-As a commodity, class context syntax allows to refer
+As a convenience, class context syntax allows to refer
   to local class operations and their global counterparts
   uniformly;  type inference resolves ambiguities.  For example:%
 \end{isamarkuptext}%