equal
deleted
inserted
replaced
8 to avoid clashes with @{text"<"} and @{text"\<le>"} in theory @{text |
8 to avoid clashes with @{text"<"} and @{text"\<le>"} in theory @{text |
9 Main}. To restrict the application of @{text"<<"} and @{text"<<="} we |
9 Main}. To restrict the application of @{text"<<"} and @{text"<<="} we |
10 introduce the class @{text ordrel}: |
10 introduce the class @{text ordrel}: |
11 *} |
11 *} |
12 |
12 |
13 axclass ordrel < "term" |
13 axclass ordrel < type |
14 |
14 |
15 text{*\noindent |
15 text{*\noindent |
16 This introduces a new class @{text ordrel} and makes it a subclass of |
16 This introduces a new class @{text ordrel} and makes it a subclass of |
17 the predefined class @{text term}, which |
17 the predefined class @{text type}, which |
18 is the class of all HOL types.\footnote{The quotes around @{text term} |
18 is the class of all HOL types. |
19 simply avoid the clash with the command \isacommand{term}.} |
|
20 This is a degenerate form of axiomatic type class without any axioms. |
19 This is a degenerate form of axiomatic type class without any axioms. |
21 Its sole purpose is to restrict the use of overloaded constants to meaningful |
20 Its sole purpose is to restrict the use of overloaded constants to meaningful |
22 instances: |
21 instances: |
23 *} |
22 *} |
24 |
23 |