equal
deleted
inserted
replaced
1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{Overloading}% |
3 \def\isabellecontext{Overloading}% |
4 \isamarkupfalse% |
4 \isamarkupfalse% |
5 \isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isachardoublequote}term{\isachardoublequote}{\isacharparenright}ordrel\isanewline |
5 \isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}ordrel\isanewline |
6 \isamarkupfalse% |
6 \isamarkupfalse% |
7 \isacommand{by}\ intro{\isacharunderscore}classes\isamarkupfalse% |
7 \isacommand{by}\ intro{\isacharunderscore}classes\isamarkupfalse% |
8 % |
8 % |
9 \begin{isamarkuptext}% |
9 \begin{isamarkuptext}% |
10 \noindent |
10 \noindent |
11 This \isacommand{instance} declaration can be read like the declaration of |
11 This \isacommand{instance} declaration can be read like the declaration of |
12 a function on types. The constructor \isa{list} maps types of class \isa{term} (all HOL types), to types of class \isa{ordrel}; |
12 a function on types. The constructor \isa{list} maps types of class \isa{type} (all HOL types), to types of class \isa{ordrel}; |
13 in other words, |
13 in other words, |
14 if \isa{ty\ {\isacharcolon}{\isacharcolon}\ term} then \isa{ty\ list\ {\isacharcolon}{\isacharcolon}\ ordrel}. |
14 if \isa{ty\ {\isacharcolon}{\isacharcolon}\ type} then \isa{ty\ list\ {\isacharcolon}{\isacharcolon}\ ordrel}. |
15 Of course we should also define the meaning of \isa{{\isacharless}{\isacharless}{\isacharequal}} and |
15 Of course we should also define the meaning of \isa{{\isacharless}{\isacharless}{\isacharequal}} and |
16 \isa{{\isacharless}{\isacharless}} on lists:% |
16 \isa{{\isacharless}{\isacharless}} on lists:% |
17 \end{isamarkuptext}% |
17 \end{isamarkuptext}% |
18 \isamarkuptrue% |
18 \isamarkuptrue% |
19 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
19 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |