author | haftmann |

Tue May 26 13:40:49 2009 +0200 (2009-05-26) | |

changeset 31255 | 0f8cb37bcafd |

parent 31254 | 03a35fbc9dc6 |

child 31256 | cf75908fd3c3 |

clarified benefit of interpretation

doc-src/Classes/Thy/Classes.thy | file | annotate | diff | revisions | |

doc-src/Classes/Thy/document/Classes.tex | file | annotate | diff | revisions |

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