src/HOL/Number_Theory/Pocklington.thy
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.