equal
deleted
inserted
replaced
|
1 (*<*)theory Overloading2 = Overloading1:(*>*) |
|
2 |
|
3 text{* |
|
4 Of course this is not the only possible definition of the two relations. |
|
5 Componentwise |
|
6 *} |
|
7 |
|
8 instance list :: (ordrel)ordrel |
|
9 by intro_classes |
|
10 |
|
11 defs (overloaded) |
|
12 le_list_def: "xs <<= (ys::'a::ordrel list) \<equiv> |
|
13 size xs = size ys \<and> (\<forall>i<size xs. xs!i <<= ys!i)" |
|
14 |
|
15 text{* |
|
16 %However, we retract the componetwise comparison of lists and return |
|
17 |
|
18 Note: only one definition because based on name. |
|
19 *} |
|
20 (*<*)end(*>*) |
|
21 |