2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-06-11 Thomas Sewell 2014-06-11 Hypsubst preserves equality hypotheses Fixes included for various theories affected by this change.
2014-06-28 haftmann 2014-06-28 fact consolidation
2013-08-18 wenzelm 2013-08-18 more symbols;
2011-11-13 huffman 2011-11-13 remove unnecessary number-representation-specific rules from metis calls; speed up another proof
2011-09-06 huffman 2011-09-06 avoid using legacy theorem names
2011-01-13 wenzelm 2011-01-13 eliminated global prems; tuned proofs;
2010-11-28 nipkow 2010-11-28 gave more standard finite set rules simp and intro attribute
2010-08-06 wenzelm 2010-08-06 modernized specifications; tuned headers;
2010-03-03 krauss 2010-03-03 fix fragile proof using old induction rule (cf. bdf8ad377877)
2009-09-01 haftmann 2009-09-01 some reorganization of number theory