#29 (Feb 22, 2016, 11:08:08 AM)

1. generalize more theorems to support enat and ennreal (detail / hgweb)
2. moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add (detail / hgweb)
3. 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. (detail / hgweb)
4. add extended nonnegative real numbers (detail / hgweb)
5. remove lattice syntax from countable complete lattice (detail / hgweb)
6. add countable complete lattices (detail / hgweb)
7. Borel_Space.borel is now in the type class locale (detail / hgweb)
8. add tendsto_add_ereal_nonneg (detail / hgweb)
9. add transfer rule for countable (detail / hgweb)
10. instantiate topologies for nat, int and enat (detail / hgweb)
11. add type class for topological monoids (detail / hgweb)
12. move product topology to HOL-Complex_Main (detail / hgweb)

Started by an SCM change