src/HOL/Library/Set_Algebras.thy
2015-11-05 wenzelm 2015-11-05 isabelle update_cartouches -c -t;
2015-10-06 wenzelm 2015-10-06 fewer aliases for toplevel theorem statements;
2015-07-06 wenzelm 2015-07-06 tuned proofs;
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-05-07 wenzelm 2014-05-07 more symbols; tuned proofs;
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
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