clarified benefit of interpretation
authorhaftmann
Tue May 26 13:40:49 2009 +0200 (2009-05-26)
changeset 312550f8cb37bcafd
parent 31254 03a35fbc9dc6
child 31256 cf75908fd3c3
clarified benefit of interpretation
doc-src/Classes/Thy/Classes.thy
doc-src/Classes/Thy/document/Classes.tex
     1.1 --- a/doc-src/Classes/Thy/Classes.thy	Tue May 26 12:31:01 2009 +0200
     1.2 +++ b/doc-src/Classes/Thy/Classes.thy	Tue May 26 13:40:49 2009 +0200
     1.3 @@ -485,14 +485,23 @@
     1.4    qed
     1.5  qed intro_locales
     1.6  
     1.7 +text {*
     1.8 +  \noindent This pattern is also helpful to reuse abstract
     1.9 +  specifications on the \emph{same} type.  For example, think of a
    1.10 +  class @{text preorder}; for type @{typ nat}, there are at least two
    1.11 +  possible instances: the natural order or the order induced by the
    1.12 +  divides relation.  But only one of these instances can be used for
    1.13 +  @{command instantiation}; using the locale behind the class @{text
    1.14 +  preorder}, it is still possible to utilise the same abstract
    1.15 +  specification again using @{command interpretation}.
    1.16 +*}
    1.17  
    1.18  subsection {* Additional subclass relations *}
    1.19  
    1.20  text {*
    1.21 -  Any @{text "group"} is also a @{text "monoid"};  this
    1.22 -  can be made explicit by claiming an additional
    1.23 -  subclass relation,
    1.24 -  together with a proof of the logical difference:
    1.25 +  Any @{text "group"} is also a @{text "monoid"}; this can be made
    1.26 +  explicit by claiming an additional subclass relation, together with
    1.27 +  a proof of the logical difference:
    1.28  *}
    1.29  
    1.30  subclass %quote (in group) monoid
    1.31 @@ -559,7 +568,7 @@
    1.32  subsection {* A note on syntax *}
    1.33  
    1.34  text {*
    1.35 -  As a commodity, class context syntax allows to refer
    1.36 +  As a convenience, class context syntax allows to refer
    1.37    to local class operations and their global counterparts
    1.38    uniformly;  type inference resolves ambiguities.  For example:
    1.39  *}
     2.1 --- a/doc-src/Classes/Thy/document/Classes.tex	Tue May 26 12:31:01 2009 +0200
     2.2 +++ b/doc-src/Classes/Thy/document/Classes.tex	Tue May 26 13:40:49 2009 +0200
     2.3 @@ -922,15 +922,25 @@
     2.4  %
     2.5  \endisadelimquote
     2.6  %
     2.7 +\begin{isamarkuptext}%
     2.8 +\noindent This pattern is also helpful to reuse abstract
     2.9 +  specifications on the \emph{same} type.  For example, think of a
    2.10 +  class \isa{preorder}; for type \isa{nat}, there are at least two
    2.11 +  possible instances: the natural order or the order induced by the
    2.12 +  divides relation.  But only one of these instances can be used for
    2.13 +  \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}; using the locale behind the class \isa{preorder}, it is still possible to utilise the same abstract
    2.14 +  specification again using \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}.%
    2.15 +\end{isamarkuptext}%
    2.16 +\isamarkuptrue%
    2.17 +%
    2.18  \isamarkupsubsection{Additional subclass relations%
    2.19  }
    2.20  \isamarkuptrue%
    2.21  %
    2.22  \begin{isamarkuptext}%
    2.23 -Any \isa{group} is also a \isa{monoid};  this
    2.24 -  can be made explicit by claiming an additional
    2.25 -  subclass relation,
    2.26 -  together with a proof of the logical difference:%
    2.27 +Any \isa{group} is also a \isa{monoid}; this can be made
    2.28 +  explicit by claiming an additional subclass relation, together with
    2.29 +  a proof of the logical difference:%
    2.30  \end{isamarkuptext}%
    2.31  \isamarkuptrue%
    2.32  %
    2.33 @@ -1038,7 +1048,7 @@
    2.34  \isamarkuptrue%
    2.35  %
    2.36  \begin{isamarkuptext}%
    2.37 -As a commodity, class context syntax allows to refer
    2.38 +As a convenience, class context syntax allows to refer
    2.39    to local class operations and their global counterparts
    2.40    uniformly;  type inference resolves ambiguities.  For example:%
    2.41  \end{isamarkuptext}%