src/HOL/Old_Number_Theory/Legacy_GCD.thy
Thu, 30 Oct 2014 21:02:01 +0100 haftmann more simp rules concerning dvd and even/odd
Tue, 07 Oct 2014 23:29:43 +0200 wenzelm more bibtex entries;
Sat, 05 Jul 2014 11:01:53 +0200 haftmann prefer ac_simps collections over separate name bindings for add and mult
Fri, 04 Jul 2014 20:18:47 +0200 haftmann reduced name variants for assoc and commute on plus and mult
Tue, 27 Mar 2012 15:40:11 +0200 huffman remove redundant lemma
Thu, 27 Oct 2011 07:46:57 +0200 huffman 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
Wed, 07 Sep 2011 09:02:58 -0700 huffman avoid using legacy theorem names
Thu, 13 Jan 2011 23:50:16 +0100 wenzelm eliminated global prems;
Fri, 06 Aug 2010 12:37:00 +0200 wenzelm modernized specifications;
Mon, 12 Jul 2010 08:58:13 +0200 haftmann dropped superfluous [code del]s
Sun, 10 Jan 2010 18:43:45 +0100 berghofe Adapted to changes in induct method.
Fri, 13 Nov 2009 14:14:04 +0100 nipkow renamed lemmas "anti_sym" -> "antisym"
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Tue, 01 Sep 2009 15:39:33 +0200 haftmann some reorganization of number theory
less more (0) tip