src/HOL/Library/Set_Algebras.thy
Mon, 17 Oct 2016 11:46:22 +0200 nipkow setsum -> sum
Fri, 12 Aug 2016 17:53:55 +0200 wenzelm more symbols;
Wed, 13 Jul 2016 20:47:56 +0200 wenzelm misc tuning and modernization;
Wed, 13 Jul 2016 14:28:15 +0200 wenzelm misc tuning and modernization;
Thu, 05 Nov 2015 10:39:49 +0100 wenzelm isabelle update_cartouches -c -t;
Tue, 06 Oct 2015 15:14:28 +0200 wenzelm fewer aliases for toplevel theorem statements;
Mon, 06 Jul 2015 22:57:34 +0200 wenzelm tuned proofs;
Wed, 17 Jun 2015 11:03:05 +0200 wenzelm isabelle update_cartouches;
Sun, 02 Nov 2014 17:20:45 +0100 wenzelm modernized header;
Sat, 05 Jul 2014 11:01:53 +0200 haftmann prefer ac_simps collections over separate name bindings for add and mult
Fri, 04 Jul 2014 20:18:47 +0200 haftmann reduced name variants for assoc and commute on plus and mult
Wed, 07 May 2014 14:44:07 +0200 wenzelm more symbols;
Fri, 01 Nov 2013 18:51:14 +0100 haftmann more simplification rules on unary and binary minus
Thu, 12 Sep 2013 09:33:36 -0700 huffman new lemmas
Thu, 12 Apr 2012 23:15:34 +0200 krauss distributivity of * over Un and UNION
Thu, 12 Apr 2012 23:07:01 +0200 krauss Set_Algebras: removed syntax \<oplus> and \<otimes>, in favour of plain + and *
Thu, 12 Apr 2012 22:55:11 +0200 krauss removed "setsum_set", now subsumed by generic setsum
Thu, 12 Apr 2012 19:58:59 +0200 krauss backported Set_Algebras to use type classes (basically reverting b3e8d5ec721d from 2008)
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Wed, 10 Aug 2011 18:02:16 -0700 huffman avoid warnings about duplicate rules
Thu, 02 Dec 2010 16:45:28 +0100 hoelzl Prove rel_interior_convex_hull_union (by Grechuck Bogdan).
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Tue, 07 Sep 2010 10:05:19 +0200 nipkow expand_fun_eq -> ext_iff
Fri, 20 Aug 2010 17:48:30 +0200 haftmann split and enriched theory SetsAndFunctions
less more (0) tip