src/HOL/Old_Number_Theory/Legacy_GCD.thy
2014-10-30 haftmann 2014-10-30 more simp rules concerning dvd and even/odd
2014-10-07 wenzelm 2014-10-07 more bibtex entries; more antiquotations;
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
2012-03-27 huffman 2012-03-27 remove redundant lemma
2011-10-27 huffman 2011-10-27 fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left
2011-09-07 huffman 2011-09-07 avoid using legacy theorem names
2011-01-13 wenzelm 2011-01-13 eliminated global prems; tuned proofs;
2010-08-06 wenzelm 2010-08-06 modernized specifications; tuned headers;
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-01-10 berghofe 2010-01-10 Adapted to changes in induct method.
2009-11-13 nipkow 2009-11-13 renamed lemmas "anti_sym" -> "antisym"
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-09-01 haftmann 2009-09-01 some reorganization of number theory