equal
deleted
inserted
replaced
25 intro: order_trans split:precedence.splits) |
25 intro: order_trans split:precedence.splits) |
26 end |
26 end |
27 |
27 |
28 instance precedence :: preorder .. |
28 instance precedence :: preorder .. |
29 |
29 |
30 instance precedence :: linorder proof |
30 instance precedence :: linorder |
|
31 proof |
31 qed (auto simp: precedence_le_def precedence_less_def |
32 qed (auto simp: precedence_le_def precedence_less_def |
32 intro: order_trans split:precedence.splits) |
33 intro: order_trans split:precedence.splits) |
33 |
34 |
|
35 instantiation precedence :: zero |
|
36 begin |
|
37 |
|
38 definition Zero_precedence_def: |
|
39 "0 = Prc 0 0" |
|
40 |
|
41 instance .. |
|
42 |
34 end |
43 end |
|
44 |
|
45 end |