src/HOL/Number_Theory/Cong.thy
Sat, 05 Jan 2019 17:24:33 +0100 wenzelm isabelle update -u control_cartouches;
Sun, 29 Jul 2018 23:04:22 +0100 paulson de-applying and removal of obsolete aliases
Sat, 02 Dec 2017 16:50:53 +0000 haftmann generalized more lemmas
Thu, 23 Nov 2017 17:03:27 +0000 haftmann generalized more lemmas
Thu, 23 Nov 2017 17:03:26 +0000 haftmann tuned
Thu, 23 Nov 2017 17:03:21 +0000 haftmann tuned and generalized
Sat, 11 Nov 2017 18:41:08 +0000 haftmann dedicated definition for coprimality
Tue, 31 Oct 2017 07:11:03 +0000 haftmann removed ancient nat-int transfer
Fri, 20 Oct 2017 20:57:55 +0200 haftmann algebraic foundation for congruences
Mon, 09 Oct 2017 19:10:48 +0200 haftmann tuned proofs
Sun, 08 Oct 2017 22:28:22 +0200 haftmann euclidean rings need no normalization
Fri, 18 Aug 2017 20:47:47 +0200 wenzelm session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
Tue, 08 Aug 2017 22:33:21 +0200 wenzelm misc tuning and modernization;
Thu, 06 Apr 2017 21:37:13 +0200 haftmann session containing computational algebra
Sat, 17 Dec 2016 15:22:14 +0100 haftmann reoriented congruence rules in non-explosive direction
Mon, 17 Oct 2016 17:33:07 +0200 nipkow setprod -> prod
Mon, 17 Oct 2016 11:46:22 +0200 nipkow setsum -> sum
Fri, 16 Sep 2016 21:28:09 +0200 wenzelm more symbols;
Thu, 26 May 2016 17:51:22 +0200 wenzelm isabelle update_cartouches -c -t;
Fri, 13 May 2016 20:24:10 +0200 wenzelm eliminated use of empty "assms";
Fri, 26 Feb 2016 22:15:09 +0100 Manuel Eberl Tuned Euclidean Rings/GCD rings
Wed, 17 Feb 2016 21:51:58 +0100 haftmann dropped various legacy fact bindings and tuned proofs
Wed, 17 Feb 2016 21:51:57 +0100 haftmann cleansed junk-producing interpretations for gcd/lcm on nat altogether
Wed, 17 Feb 2016 21:51:57 +0100 haftmann dropped various legacy fact bindings
Mon, 28 Dec 2015 19:23:15 +0100 wenzelm more symbols;
Wed, 08 Jul 2015 14:01:41 +0200 haftmann avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
Fri, 19 Jun 2015 21:41:33 +0200 wenzelm isabelle update_cartouches;
Mon, 23 Mar 2015 19:05:14 +0100 haftmann distributivity of partial minus establishes desired properties of dvd in semirings
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
Mon, 17 Nov 2014 14:55:34 +0100 haftmann generalized lemmas and tuned proofs
Fri, 07 Nov 2014 22:33:54 +0100 wenzelm tuned syntax -- separate tokens;
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Sat, 01 Nov 2014 14:20:38 +0100 wenzelm eliminated spurious semicolons;
Tue, 07 Oct 2014 23:29:43 +0200 wenzelm more bibtex entries;
Fri, 04 Jul 2014 20:18:47 +0200 haftmann reduced name variants for assoc and commute on plus and mult
Sat, 28 Jun 2014 09:16:42 +0200 haftmann fact consolidation
Sun, 09 Feb 2014 19:10:12 +0000 paulson tidied messy proofs
Wed, 05 Feb 2014 17:06:11 +0000 paulson Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
Tue, 04 Feb 2014 21:28:38 +0000 paulson Restoration of Pocklington.thy. Tidying.
Sun, 02 Feb 2014 19:15:25 +0000 paulson Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
Wed, 29 Jan 2014 15:40:33 +0000 paulson minor adjustments
Fri, 24 Jan 2014 15:21:00 +0000 paulson Restored Suc rather than +1, and using Library/Binimial
Tue, 19 Nov 2013 10:05:53 +0100 haftmann eliminiated neg_numeral in favour of - (numeral _)
Fri, 01 Nov 2013 18:51:14 +0100 haftmann more simplification rules on unary and binary minus
Tue, 27 Mar 2012 15:53:48 +0200 huffman remove redundant lemma
Sat, 10 Sep 2011 23:27:32 +0200 wenzelm misc tuning;
Sun, 13 Mar 2011 22:55:50 +0100 wenzelm tuned headers;
Thu, 13 Jan 2011 23:50:16 +0100 wenzelm eliminated global prems;
Wed, 02 Jun 2010 16:24:14 +0200 haftmann avoid duplicate import
Mon, 26 Apr 2010 11:34:19 +0200 haftmann dropped group_simps, ring_simps, field_eq_simps
Mon, 08 Mar 2010 09:38:58 +0100 haftmann transfer: avoid camel case
Mon, 16 Nov 2009 17:22:10 +0000 webertj Fixed a typo in a comment.
Tue, 01 Sep 2009 15:39:33 +0200 haftmann some reorganization of number theory
less more (0) tip