src/HOL/Number_Theory/Residues.thy
Mon, 22 May 2017 14:08:22 +0200 wenzelm removed junk;
Thu, 04 May 2017 16:49:29 +0200 eberlm More material on totient function
Wed, 12 Apr 2017 09:27:43 +0200 haftmann more fundamental euler's totient function on nat rather than int;
Thu, 06 Apr 2017 08:33:37 +0200 haftmann more approproiate placement of theories MiscAlgebra and Multiplicate_Group
Tue, 28 Feb 2017 15:17:57 +0000 paulson tidied some messy proofs
Sat, 17 Dec 2016 15:22:14 +0100 haftmann reoriented congruence rules in non-explosive direction
Mon, 17 Oct 2016 15:20:06 +0200 eberlm Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
Mon, 17 Oct 2016 17:33:07 +0200 nipkow setprod -> prod
Mon, 08 Aug 2016 17:47:51 +0200 eberlm is_prime -> prime
Fri, 22 Jul 2016 17:35:54 +0200 eberlm Removed redundant material related to primes
Thu, 21 Jul 2016 10:06:04 +0200 eberlm Overhaul of prime/multiplicity/prime_factors
Sat, 09 Jul 2016 13:26:16 +0200 haftmann more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
Thu, 26 May 2016 17:51:22 +0200 wenzelm isabelle update_cartouches -c -t;
Wed, 17 Feb 2016 21:51:57 +0100 haftmann dropped various legacy fact bindings
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 23:51:30 +0200 wenzelm tuned;
Fri, 19 Jun 2015 23:40:46 +0200 wenzelm tuned proofs;
Fri, 19 Jun 2015 21:41:33 +0200 wenzelm isabelle update_cartouches;
Mon, 16 Mar 2015 15:30:00 +0000 paulson The factorial function, "fact", now has type "nat => 'a"
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, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
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
Thu, 06 Feb 2014 23:09:22 +0000 paulson tidied
Mon, 03 Feb 2014 00:22:48 +0000 paulson fixed indentation
Sun, 02 Feb 2014 21:48:28 +0000 paulson new lemmas involving phi from Lehmer AFP entry
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.
Sat, 01 Feb 2014 00:32:32 +0000 paulson version of Fermat's Theorem for type nat
Thu, 30 Jan 2014 10:00:53 +0100 haftmann more direct simplification rules for 1 div/mod numeral;
Wed, 29 Jan 2014 15:40:33 +0000 paulson minor adjustments
Fri, 29 Nov 2013 08:26:45 +0100 traytel set_comprehension_pointfree simproc causes to many surprises if enabled by default
Tue, 19 Nov 2013 10:05:53 +0100 haftmann eliminiated neg_numeral in favour of - (numeral _)
Thu, 08 Nov 2012 11:59:48 +0100 bulwahn adjusting proofs as the set_comprehension_pointfree simproc breaks some existing proofs
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;
Mon, 26 Apr 2010 11:34:19 +0200 haftmann dropped group_simps, ring_simps, field_eq_simps
Mon, 01 Mar 2010 13:40:23 +0100 haftmann replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
Tue, 01 Sep 2009 15:39:33 +0200 haftmann some reorganization of number theory
less more (0) tip