src/HOL/Library/Lattice_Algebras.thy
2017-03-08 wenzelm 2017-03-08 tuned proofs;
2015-11-02 wenzelm 2015-11-02 tuned whitespace;
2015-07-09 wenzelm 2015-07-09 tuned proofs;
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-08-05 wenzelm 2014-08-05 tuned proofs;
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-03-20 wenzelm 2014-03-20 tuned proofs;
2013-12-25 haftmann 2013-12-25 prefer more canonical names for lemmas on min/max
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-08-27 wenzelm 2013-08-27 tuned proofs;
2012-03-17 wenzelm 2012-03-17 tuned proofs;
2011-01-12 wenzelm 2011-01-12 eliminated global prems; tuned proofs;
2010-07-19 haftmann 2010-07-19 discontinued pretending that abel_cancel is logic-independent; cleaned up junk
2010-05-17 huffman 2010-05-17 simplify proof
2010-03-18 blanchet 2010-03-18 now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
2010-02-08 haftmann 2010-02-08 separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4