src/HOL/Library/Boolean_Algebra.thy
2017-04-01 wenzelm 2017-04-01 tuned proofs;
2016-07-12 wenzelm 2016-07-12 misc tuning and modernization;
2015-11-09 wenzelm 2015-11-09 qualifier is mandatory by default;
2015-08-06 wenzelm 2015-08-06 tuned;
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header;
2013-12-27 haftmann 2013-12-27 prefer target-style syntaxx for sublocale
2010-01-28 haftmann 2010-01-28 dropped mk_left_commute; use interpretation of locale abel_semigroup instead
2009-03-23 haftmann 2009-03-23 Main is (Complex_Main) base entry point in library theories
2009-02-19 huffman 2009-02-19 declare xor_compl_{left,right} [simp]
2009-01-26 haftmann 2009-01-26 tuned header
2008-06-26 haftmann 2008-06-26 established Plain theory and image
2007-12-18 haftmann 2007-12-18 switched from PreList to ATP_Linkup
2007-12-10 haftmann 2007-12-10 switched import from Main to PreList
2007-11-05 ballarin 2007-11-05 Type instance of thm mk_left_commute in locales.
2007-08-21 huffman 2007-08-21 declare conj_absorb [simp]
2007-08-20 huffman 2007-08-20 cleaned up; declared more simp rules
2007-08-20 kleing 2007-08-20 boolean algebras as locales and numbers as types by Brian Huffman