changeset 4640 | ac6cf9f18653 |
parent 3947 | eb707467f8c5 |
child 5889 | d3ecef6b5682 |
4639:bc6e2936a293 | 4640:ac6cf9f18653 |
---|---|
43 order_refl "x <= x" |
43 order_refl "x <= x" |
44 order_trans "[| x <= y; y <= z |] ==> x <= z" |
44 order_trans "[| x <= y; y <= z |] ==> x <= z" |
45 order_antisym "[| x <= y; y <= x |] ==> x = y" |
45 order_antisym "[| x <= y; y <= x |] ==> x = y" |
46 order_less_le "x < y = (x <= y & x ~= y)" |
46 order_less_le "x < y = (x <= y & x ~= y)" |
47 |
47 |
48 axclass linorder < order |
|
49 linorder_linear "x <= y | y <= x" |
|
50 |
|
48 end |
51 end |