src/HOL/GCD.thy
Fri, 19 Oct 2012 15:12:52 +0200 webertj Renamed {left,right}_distrib to distrib_{right,left}.
Fri, 27 Jul 2012 19:57:23 +0200 wenzelm tuned proofs -- avoid odd situations of polymorphic Frees in goal state;
Tue, 27 Dec 2011 09:15:26 +0100 haftmann prefer canonical fold on lists
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
Tue, 25 Oct 2011 12:00:52 +0200 huffman merge Gcd/GCD and Lcm/LCM
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Fri, 09 Sep 2011 00:22:18 +0200 krauss added syntactic classes for "inf" and "sup"
Wed, 07 Sep 2011 09:02:58 -0700 huffman avoid using legacy theorem names
Tue, 06 Sep 2011 19:03:41 -0700 huffman avoid using legacy theorem names
Thu, 18 Aug 2011 13:55:26 +0200 haftmann observe distinction between sets and predicates more properly
Fri, 20 May 2011 11:44:16 +0200 haftmann names of fold_set locales resemble name of characteristic property more closely
Mon, 21 Feb 2011 10:44:19 +0100 blanchet renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
Fri, 14 Jan 2011 15:44:47 +0100 wenzelm eliminated global prems;
Mon, 12 Jul 2010 11:39:27 +0200 haftmann avoid explicit mandatory prefix markers when prefixes are mandatory implicitly
Mon, 26 Apr 2010 11:34:19 +0200 haftmann dropped group_simps, ring_simps, field_eq_simps
Thu, 11 Mar 2010 14:39:58 +0100 haftmann tuned prefixes of ac interpretations
Mon, 08 Mar 2010 09:38:58 +0100 haftmann transfer: avoid camel case
Wed, 24 Feb 2010 14:19:53 +0100 haftmann crossproduct coprimality lemmas
Thu, 18 Feb 2010 14:21:44 -0800 huffman get rid of many duplicate simp rule warnings
Fri, 05 Feb 2010 14:33:50 +0100 haftmann more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
Thu, 28 Jan 2010 11:48:43 +0100 haftmann dropped mk_left_commute; use interpretation of locale abel_semigroup instead
Sun, 10 Jan 2010 18:43:45 +0100 berghofe Adapted to changes in induct method.
Fri, 01 Jan 2010 19:15:43 +0100 nipkow added lemmas
Fri, 01 Jan 2010 17:21:44 +0100 nipkow added lemma
Fri, 01 Jan 2010 16:34:51 +0100 nipkow removed FIXME
Tue, 08 Dec 2009 13:40:57 +0100 haftmann resorted code equations from "old" number theory version
Fri, 04 Dec 2009 08:52:09 +0100 nipkow removed redundant lemma
Fri, 13 Nov 2009 14:14:04 +0100 nipkow renamed lemmas "anti_sym" -> "antisym"
Thu, 29 Oct 2009 11:41:36 +0100 haftmann moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
Fri, 23 Oct 2009 18:59:24 +0200 blanchet continuation of Nitpick's integration into Isabelle;
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Tue, 06 Oct 2009 15:51:34 +0200 haftmann added syntactic Inf and Sup
Tue, 01 Sep 2009 15:39:33 +0200 haftmann some reorganization of number theory
Wed, 26 Aug 2009 19:54:01 +0200 nipkow got rid of complicated class finite_intvl_succ and defined "upto" directly on int, the only instance of the class.
Tue, 21 Jul 2009 14:08:58 +0200 nipkow Made dvd/gcd/lcm a complete lattice by introducing Gcd/GCD/Lcm/LCM
Tue, 21 Jul 2009 11:01:07 +0200 nipkow Tests for executability of "prime"
Fri, 17 Jul 2009 10:07:15 +0200 berghofe merged
Tue, 14 Jul 2009 17:18:51 +0200 berghofe merged
Fri, 10 Jul 2009 10:45:30 -0400 avigad Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
Wed, 15 Jul 2009 20:34:58 +0200 nipkow Made "prime" executable
Mon, 13 Jul 2009 19:07:05 +0200 berghofe Tuned proof of lcm_1_iff_int, because metis produced enormous proof term.
Sun, 12 Jul 2009 14:48:01 +0200 nipkow more gcd/lcm lemmas
Sun, 12 Jul 2009 10:14:51 +0200 nipkow More about gcd/lcm, and some cleaning up
Tue, 07 Jul 2009 17:39:51 +0200 nipkow renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
Fri, 26 Jun 2009 19:44:39 +0200 nipkow lcm abs lemmas
Fri, 26 Jun 2009 10:46:33 +0200 nipkow gcd abs lemmas
Thu, 25 Jun 2009 07:34:12 +0200 nipkow Cleaned up GCD
Tue, 23 Jun 2009 12:58:53 +0200 nipkow new lemmas
Sun, 21 Jun 2009 23:04:37 +0200 nipkow new lemmas
Sat, 20 Jun 2009 13:34:54 +0200 nipkow added lemmas; tuned
Sat, 20 Jun 2009 01:53:39 +0200 nipkow new lemmas and tuning
Thu, 18 Jun 2009 07:46:30 -0700 huffman more [code del] declarations
Wed, 17 Jun 2009 16:55:01 -0700 huffman new GCD library, courtesy of Jeremy Avigad
Fri, 27 Mar 2009 10:05:11 +0100 haftmann normalized imports
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Tue, 24 Feb 2009 11:12:58 -0800 huffman make more proofs work whether or not One_nat_def is a simp rule
Sat, 21 Feb 2009 20:52:30 +0100 nipkow Removed subsumed lemmas
Sat, 31 Jan 2009 09:04:16 +0100 nipkow added some simp rules
Wed, 28 Jan 2009 11:03:42 +0100 haftmann Plain, Main form meeting points in import hierarchy
less more (0) -60 tip