# 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}%