equal
deleted
inserted
replaced
3 subsubsection{*Controlled Overloading with Type Classes*} |
3 subsubsection{*Controlled Overloading with Type Classes*} |
4 |
4 |
5 text{* |
5 text{* |
6 We now start with the theory of ordering relations, which we shall phrase |
6 We now start with the theory of ordering relations, which we shall phrase |
7 in terms of the two binary symbols @{text"<<"} and @{text"<<="} |
7 in terms of the two binary symbols @{text"<<"} and @{text"<<="} |
8 to avoid clashes with @{text"<"} and @{text"\<le>"} in theory @{text |
8 to avoid clashes with @{text"<"} and @{text"<="} 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 < type |
13 axclass ordrel < type |