src/HOL/Library/Function_Algebras.thy
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