src/HOL/Number_Theory/Pocklington.thy
Mon, 04 Feb 2019 12:16:03 +0100 Manuel Eberl More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Mon, 24 Sep 2018 14:30:09 +0200 nipkow Prefix form of infix with * on either side no longer needs special treatment
Sun, 29 Jul 2018 23:04:22 +0100 paulson de-applying and removal of obsolete aliases
Sat, 12 May 2018 22:20:46 +0200 haftmann removed some non-essential rules
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Sat, 06 Jan 2018 13:05:25 +0100 nipkow tuned op's
Sun, 26 Nov 2017 21:08:32 +0100 wenzelm more symbols;
Sat, 11 Nov 2017 18:41:08 +0000 haftmann dedicated definition for coprimality
Fri, 20 Oct 2017 20:57:55 +0200 haftmann algebraic foundation for congruences
Tue, 01 Aug 2017 22:19:37 +0200 wenzelm misc tuning and modernization;
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
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)
Sun, 16 Oct 2016 09:31:05 +0200 haftmann more standardized theorem names for facts involving the div and mod identity
Fri, 16 Sep 2016 12:30:55 +0200 haftmann prefer abbreviation for trivial set conversion
Fri, 09 Sep 2016 15:12:40 +0200 nipkow msetsum -> set_mset, msetprod -> prod_mset
Mon, 08 Aug 2016 17:47:51 +0200 eberlm is_prime -> prime
Thu, 21 Jul 2016 10:06:04 +0200 eberlm Overhaul of prime/multiplicity/prime_factors
Fri, 26 Feb 2016 22:15:09 +0100 Manuel Eberl Tuned Euclidean Rings/GCD rings
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
Tue, 01 Dec 2015 14:09:10 +0000 paulson Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
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;
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
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
Sun, 09 Feb 2014 17:47:23 +0100 wenzelm minimal document;
Thu, 06 Feb 2014 13:04:06 +0000 paulson fixed problem (?) by deleting "thm" line
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.
less more (0) tip