equal
deleted
inserted
replaced
920 % |
920 % |
921 \isadelimquote |
921 \isadelimquote |
922 % |
922 % |
923 \endisadelimquote |
923 \endisadelimquote |
924 % |
924 % |
|
925 \begin{isamarkuptext}% |
|
926 \noindent This pattern is also helpful to reuse abstract |
|
927 specifications on the \emph{same} type. For example, think of a |
|
928 class \isa{preorder}; for type \isa{nat}, there are at least two |
|
929 possible instances: the natural order or the order induced by the |
|
930 divides relation. But only one of these instances can be used for |
|
931 \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}; using the locale behind the class \isa{preorder}, it is still possible to utilise the same abstract |
|
932 specification again using \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}.% |
|
933 \end{isamarkuptext}% |
|
934 \isamarkuptrue% |
|
935 % |
925 \isamarkupsubsection{Additional subclass relations% |
936 \isamarkupsubsection{Additional subclass relations% |
926 } |
937 } |
927 \isamarkuptrue% |
938 \isamarkuptrue% |
928 % |
939 % |
929 \begin{isamarkuptext}% |
940 \begin{isamarkuptext}% |
930 Any \isa{group} is also a \isa{monoid}; this |
941 Any \isa{group} is also a \isa{monoid}; this can be made |
931 can be made explicit by claiming an additional |
942 explicit by claiming an additional subclass relation, together with |
932 subclass relation, |
943 a proof of the logical difference:% |
933 together with a proof of the logical difference:% |
|
934 \end{isamarkuptext}% |
944 \end{isamarkuptext}% |
935 \isamarkuptrue% |
945 \isamarkuptrue% |
936 % |
946 % |
937 \isadelimquote |
947 \isadelimquote |
938 % |
948 % |
1036 \isamarkupsubsection{A note on syntax% |
1046 \isamarkupsubsection{A note on syntax% |
1037 } |
1047 } |
1038 \isamarkuptrue% |
1048 \isamarkuptrue% |
1039 % |
1049 % |
1040 \begin{isamarkuptext}% |
1050 \begin{isamarkuptext}% |
1041 As a commodity, class context syntax allows to refer |
1051 As a convenience, class context syntax allows to refer |
1042 to local class operations and their global counterparts |
1052 to local class operations and their global counterparts |
1043 uniformly; type inference resolves ambiguities. For example:% |
1053 uniformly; type inference resolves ambiguities. For example:% |
1044 \end{isamarkuptext}% |
1054 \end{isamarkuptext}% |
1045 \isamarkuptrue% |
1055 \isamarkuptrue% |
1046 % |
1056 % |