src/HOL/GCD.thy
Tue, 02 Jun 2015 09:10:05 +0200 wenzelm tuned proof;
Thu, 30 Apr 2015 15:28:01 +0100 paulson tidying some messy proofs
Wed, 08 Apr 2015 21:48:59 +0200 wenzelm eliminated hard tabs;
Wed, 25 Mar 2015 10:44:57 +0100 wenzelm prefer local fixes;
Tue, 10 Mar 2015 15:20:40 +0000 paulson Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
Sun, 15 Feb 2015 17:01:22 +0100 haftmann explicit equivalence for strict order on lattices
Tue, 10 Feb 2015 14:29:36 +0100 wenzelm indicate slow proof (approx. 20s);
Mon, 17 Nov 2014 14:55:32 +0100 haftmann formally self-contained gcd type classes
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Thu, 30 Oct 2014 21:02:01 +0100 haftmann more simp rules concerning dvd and even/odd
Sun, 26 Oct 2014 19:11:16 +0100 haftmann eliminated redundancies;
Fri, 24 Oct 2014 15:07:51 +0200 hoelzl use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
Thu, 23 Oct 2014 14:04:05 +0200 haftmann downshift of theory Parity in the hierarchy
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
Wed, 19 Mar 2014 18:47:22 +0100 haftmann elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
Sun, 16 Mar 2014 18:09:04 +0100 haftmann normalising simp rules for compound operators
Thu, 26 Dec 2013 22:47:49 +0100 haftmann prefer ephemeral interpretation over interpretation in proof contexts;
Tue, 19 Nov 2013 10:05:53 +0100 haftmann eliminiated neg_numeral in favour of - (numeral _)
Fri, 15 Nov 2013 22:02:01 +0100 haftmann proper code equations for Gcd and Lcm on nat and int
Tue, 05 Nov 2013 09:44:57 +0100 hoelzl generalize SUP and INF to the syntactic type classes Sup and Inf
Thu, 25 Jul 2013 08:57:16 +0200 haftmann factored syntactic type classes for bot and top (by Alessandro Coglio)
Wed, 19 Jun 2013 17:33:51 +0200 noschinl added coprimality lemma
Tue, 26 Mar 2013 22:09:39 +0100 haftmann avoid odd foundational terms after interpretation;
Sat, 23 Mar 2013 20:50:39 +0100 haftmann fundamental revision of big operators on sets
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.
less more (0) -60 tip