src/HOL/Library/Function_Algebras.thy
2016-02-10 hoelzl 2016-02-10 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.
2015-07-06 wenzelm 2015-07-06 tuned proofs;
2015-06-23 paulson 2015-06-23 Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2015-03-23 haftmann 2015-03-23 explicit commutative additive inverse operation; more explicit focal point for commutative monoids with an inverse operation
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-05-02 wenzelm 2014-05-02 tuned spelling;
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-03-23 haftmann 2013-03-23 fundamental revision of big operators on sets
2012-07-02 haftmann 2012-07-02 eta-expanded occurences of algebraic functionals are simplified by default
2012-02-21 wenzelm 2012-02-21 misc tuning; more indentation;
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-08-23 haftmann 2010-08-23 dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
2010-08-20 haftmann 2010-08-20 split and enriched theory SetsAndFunctions