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