equal
deleted
inserted
replaced
8 |
8 |
9 Ord = HOL + |
9 Ord = HOL + |
10 |
10 |
11 axclass |
11 axclass |
12 ord < term |
12 ord < term |
|
13 |
|
14 global |
13 |
15 |
14 syntax |
16 syntax |
15 "op <" :: ['a::ord, 'a] => bool ("op <") |
17 "op <" :: ['a::ord, 'a] => bool ("op <") |
16 "op <=" :: ['a::ord, 'a] => bool ("op <=") |
18 "op <=" :: ['a::ord, 'a] => bool ("op <=") |
17 |
19 |
26 syntax (symbols) |
28 syntax (symbols) |
27 "op <=" :: ['a::ord, 'a] => bool ("op \\<le>") |
29 "op <=" :: ['a::ord, 'a] => bool ("op \\<le>") |
28 "op <=" :: ['a::ord, 'a] => bool ("(_/ \\<le> _)" [50, 51] 50) |
30 "op <=" :: ['a::ord, 'a] => bool ("(_/ \\<le> _)" [50, 51] 50) |
29 |
31 |
30 |
32 |
|
33 local |
|
34 |
31 defs |
35 defs |
32 mono_def "mono(f) == (!A B. A <= B --> f(A) <= f(B))" |
36 mono_def "mono(f) == (!A B. A <= B --> f(A) <= f(B))" |
33 min_def "min a b == (if a <= b then a else b)" |
37 min_def "min a b == (if a <= b then a else b)" |
34 max_def "max a b == (if a <= b then b else a)" |
38 max_def "max a b == (if a <= b then b else a)" |
35 Least_def "Least P == @x. P(x) & (ALL y. P(y) --> x <= y)" |
39 Least_def "Least P == @x. P(x) & (ALL y. P(y) --> x <= y)" |