Summary
- generalize more theorems to support enat and ennreal
- moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
- Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
- add extended nonnegative real numbers
- remove lattice syntax from countable complete lattice
- add countable complete lattices
- Borel_Space.borel is now in the type class locale
- add tendsto_add_ereal_nonneg
- add transfer rule for countable
- instantiate topologies for nat, int and enat
- add type class for topological monoids
- move product topology to HOL-Complex_Main