equal
deleted
inserted
replaced
1 (*<*)theory Overloading1 = Main:(*>*) |
1 (*<*)theory Overloading1 = Main:(*>*) |
2 |
2 |
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 want to phrase |
6 We now start with the theory of ordering relations, which we want to phrase |
7 in terms of the two binary symbols @{text"<<"} and @{text"<<="}: they have |
7 in terms of the two binary symbols @{text"<<"} and @{text"<<="}: they have |
8 been chosen to avoid clashes with @{text"<"} and @{text"\<le>"} in theory @{text |
8 been chosen to avoid clashes with @{text"<"} and @{text"\<le>"} in theory @{text |