- Now imports Code_Setup, rather than Set and Fun, since the theorems
about orderings are already needed in Set
- Moved "Dense orders" section to Set, since it requires set notation.
- The "Order on sets" section is no longer necessary, since it is subsumed by
the order on functions and booleans.
- Moved proofs of Least_mono and Least_equality to Set, since they require
set notation.
- In proof of "instance fun :: (type, order) order", use ext instead of
expand_fun_eq, since the latter is not yet available.
- predicate1I is no longer declared as introduction rule, since it interferes
with subsetI