15 subsection {* Order signatures and orders *} |
15 subsection {* Order signatures and orders *} |
16 |
16 |
17 axclass |
17 axclass |
18 ord < type |
18 ord < type |
19 |
19 |
20 syntax |
|
21 "less" :: "['a::ord, 'a] => bool" ("op <") |
|
22 "less_eq" :: "['a::ord, 'a] => bool" ("op <=") |
|
23 |
|
24 consts |
20 consts |
25 "less" :: "['a::ord, 'a] => bool" ("(_/ < _)" [50, 51] 50) |
21 less :: "['a::ord, 'a] => bool" |
26 "less_eq" :: "['a::ord, 'a] => bool" ("(_/ <= _)" [50, 51] 50) |
22 less_eq :: "['a::ord, 'a] => bool" |
27 |
23 |
28 syntax (xsymbols) |
24 const_syntax |
29 "less_eq" :: "['a::ord, 'a] => bool" ("op \<le>") |
25 less ("op <") |
30 "less_eq" :: "['a::ord, 'a] => bool" ("(_/ \<le> _)" [50, 51] 50) |
26 less ("(_/ < _)" [50, 51] 50) |
31 |
27 less_eq ("op <=") |
32 syntax (HTML output) |
28 less_eq ("(_/ <= _)" [50, 51] 50) |
33 "less_eq" :: "['a::ord, 'a] => bool" ("op \<le>") |
29 |
34 "less_eq" :: "['a::ord, 'a] => bool" ("(_/ \<le> _)" [50, 51] 50) |
30 const_syntax (xsymbols) |
|
31 less_eq ("op \<le>") |
|
32 less_eq ("(_/ \<le> _)" [50, 51] 50) |
|
33 |
|
34 const_syntax (HTML output) |
|
35 less_eq ("op \<le>") |
|
36 less_eq ("(_/ \<le> _)" [50, 51] 50) |
35 |
37 |
36 abbreviation (input) |
38 abbreviation (input) |
37 greater (infixl ">" 50) |
39 greater (infixl ">" 50) |
38 "x > y == y < x" |
40 "x > y == y < x" |
39 greater_eq (infixl ">=" 50) |
41 greater_eq (infixl ">=" 50) |
40 "x >= y == y <= x" |
42 "x >= y == y <= x" |
41 |
43 |
42 abbreviation (xsymbols) |
44 const_syntax (xsymbols) |
43 greater_eq1 (infixl "\<ge>" 50) |
45 greater_eq (infixl "\<ge>" 50) |
44 "x \<ge> y == x >= y" |
|
45 |
|
46 abbreviation (HTML output) |
|
47 greater_eq2 (infixl "\<ge>" 50) |
|
48 "greater_eq2 == greater_eq" |
|
49 |
46 |
50 |
47 |
51 subsection {* Monotonicity *} |
48 subsection {* Monotonicity *} |
52 |
49 |
53 locale mono = |
50 locale mono = |