2010-05-17 huffman 2010-05-17 declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)
2010-05-04 haftmann 2010-05-04 locale predicates of classes carry a mandatory "class" prefix
2010-04-20 hoelzl 2010-04-20 Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
2010-04-26 haftmann 2010-04-26 use new classes (linordered_)field_inverse_zero
2010-04-26 haftmann 2010-04-26 class division_ring_inverse_zero
2010-04-23 haftmann 2010-04-23 sharpened constraint (c.f. 4e7f5b22dd7d)
2010-04-07 Christian Urban 2010-04-07 simplified induction case in finite_psubset_induct; tuned the proof that uses this induction principle
2010-03-23 huffman 2010-03-23 sublocale comm_monoid_add < setprod --> sublocale comm_monoid_mult < setprod
2010-03-18 blanchet 2010-03-18 merged
2010-03-18 blanchet 2010-03-18 now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
2010-03-18 haftmann 2010-03-18 generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
2010-03-11 haftmann 2010-03-11 moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
2010-03-10 haftmann 2010-03-10 split off theory Big_Operators from theory Finite_Set