equal
deleted
inserted
replaced
12 in terms of the two binary symbols \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} |
12 in terms of the two binary symbols \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} |
13 to avoid clashes with \isa{{\isacharless}} and \isa{{\isasymle}} in theory \isa{Main}. To restrict the application of \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} we |
13 to avoid clashes with \isa{{\isacharless}} and \isa{{\isasymle}} in theory \isa{Main}. To restrict the application of \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} we |
14 introduce the class \isa{ordrel}:% |
14 introduce the class \isa{ordrel}:% |
15 \end{isamarkuptext}% |
15 \end{isamarkuptext}% |
16 \isamarkuptrue% |
16 \isamarkuptrue% |
17 \isacommand{axclass}\ ordrel\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isamarkupfalse% |
17 \isacommand{axclass}\ ordrel\ {\isacharless}\ type\isamarkupfalse% |
18 % |
18 % |
19 \begin{isamarkuptext}% |
19 \begin{isamarkuptext}% |
20 \noindent |
20 \noindent |
21 This introduces a new class \isa{ordrel} and makes it a subclass of |
21 This introduces a new class \isa{ordrel} and makes it a subclass of |
22 the predefined class \isa{term}, which |
22 the predefined class \isa{type}, which |
23 is the class of all HOL types.\footnote{The quotes around \isa{term} |
23 is the class of all HOL types. |
24 simply avoid the clash with the command \isacommand{term}.} |
|
25 This is a degenerate form of axiomatic type class without any axioms. |
24 This is a degenerate form of axiomatic type class without any axioms. |
26 Its sole purpose is to restrict the use of overloaded constants to meaningful |
25 Its sole purpose is to restrict the use of overloaded constants to meaningful |
27 instances:% |
26 instances:% |
28 \end{isamarkuptext}% |
27 \end{isamarkuptext}% |
29 \isamarkuptrue% |
28 \isamarkuptrue% |