src/HOL/Number_Theory/Pocklington.thy
4 months ago Manuel Eberl 2019-02-04 More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
9 months ago nipkow 2018-09-24 Prefix form of infix with * on either side no longer needs special treatment because (* and *) are no longer comment brackets in terms.
11 months ago paulson 2018-07-29 de-applying and removal of obsolete aliases
13 months ago haftmann 2018-05-12 removed some non-essential rules
17 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
17 months ago nipkow 2018-01-06 tuned op's
19 months ago wenzelm 2017-11-26 more symbols;
19 months ago haftmann 2017-11-11 dedicated definition for coprimality
20 months ago haftmann 2017-10-20 algebraic foundation for congruences
23 months ago wenzelm 2017-08-01 misc tuning and modernization;
2017-05-04 eberlm 2017-05-04 More material on totient function
2017-04-12 haftmann 2017-04-12 more fundamental euler's totient function on nat rather than int; avoid generic name phi; separate theory for euler's totient function
2017-04-06 haftmann 2017-04-06 more approproiate placement of theories MiscAlgebra and Multiplicate_Group
2016-12-17 haftmann 2016-12-17 reoriented congruence rules in non-explosive direction
2016-10-17 eberlm 2016-10-17 Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
2016-10-16 haftmann 2016-10-16 more standardized theorem names for facts involving the div and mod identity
2016-09-16 haftmann 2016-09-16 prefer abbreviation for trivial set conversion
2016-09-09 nipkow 2016-09-09 msetsum -> set_mset, msetprod -> prod_mset
2016-08-08 eberlm 2016-08-08 is_prime -> prime
2016-07-21 eberlm 2016-07-21 Overhaul of prime/multiplicity/prime_factors
2016-02-26 Manuel Eberl 2016-02-26 Tuned Euclidean Rings/GCD rings
2016-02-17 haftmann 2016-02-17 cleansed junk-producing interpretations for gcd/lcm on nat altogether
2016-02-17 haftmann 2016-02-17 dropped various legacy fact bindings
2015-12-01 paulson 2015-12-01 Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
2015-07-08 haftmann 2015-07-08 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
2015-06-19 wenzelm 2015-06-19 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-30 haftmann 2014-10-30 more simp rules concerning dvd and even/odd
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-02-09 wenzelm 2014-02-09 minimal document;
2014-02-06 paulson 2014-02-06 fixed problem (?) by deleting "thm" line
2014-02-05 paulson 2014-02-05 Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
2014-02-04 paulson 2014-02-04 Restoration of Pocklington.thy. Tidying.