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