src/HOL/Library/Set_Algebras.thy
2013-09-12 huffman 2013-09-12 new lemmas
2012-04-12 krauss 2012-04-12 distributivity of * over Un and UNION
2012-04-12 krauss 2012-04-12 Set_Algebras: removed syntax \<oplus> and \<otimes>, in favour of plain + and *
2012-04-12 krauss 2012-04-12 removed "setsum_set", now subsumed by generic setsum
2012-04-12 krauss 2012-04-12 backported Set_Algebras to use type classes (basically reverting b3e8d5ec721d from 2008)
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-08-10 huffman 2011-08-10 avoid warnings about duplicate rules
2010-12-02 hoelzl 2010-12-02 Prove rel_interior_convex_hull_union (by Grechuck Bogdan).
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-20 haftmann 2010-08-20 split and enriched theory SetsAndFunctions