src/HOL/Number_Theory/Primes.thy
2016-07-22 eberlm 2016-07-22 Tuned primes
2016-07-21 eberlm 2016-07-21 Overhaul of prime/multiplicity/prime_factors
2016-03-01 haftmann 2016-03-01 tuned bootstrap order to provide type classes in a more sensible order
2016-02-26 Manuel Eberl 2016-02-26 Tuned Euclidean Rings/GCD rings
2016-02-25 paulson 2016-02-25 partial tidy-up of Sylow's theorem
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-27 haftmann 2015-07-27 formal class for factorial (semi)rings
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;
2015-03-16 paulson 2015-03-16 The factorial function, "fact", now has type "nat => 'a"
2015-03-10 paulson 2015-03-10 renaming HOL/Fact.thy -> Binomial.thy
2015-03-10 paulson 2015-03-10 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
2014-11-09 haftmann 2014-11-09 reverted 1ebf0a1f12a4 after successful re-tuning of simp rules for divisibility
2014-11-05 nipkow 2014-11-05 reduced execution time
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-09 haftmann 2014-10-09 more foundational definition for predicate even
2014-10-07 wenzelm 2014-10-07 more bibtex entries; more antiquotations;
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-02-05 paulson 2014-02-05 Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
2014-02-02 paulson 2014-02-02 Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
2014-02-01 paulson 2014-02-01 Added material from Old_Number_Theory related to the Chinese Remainder Theorem
2014-01-31 paulson 2014-01-31 Restoring some proofs from the equivalent file in Old_Number_Theory.
2014-01-24 paulson 2014-01-24 Restored Suc rather than +1, and using Library/Binimial
2013-10-31 haftmann 2013-10-31 purely algebraic foundation for even/odd
2013-09-12 huffman 2013-09-12 remove unneeded assumption from prime_dvd_power lemmas; add iff forms of prime_dvd_power lemmas (thanks to Jason Dagit)
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-09-10 wenzelm 2011-09-10 misc tuning;
2011-09-07 huffman 2011-09-07 avoid using legacy theorem names
2010-11-09 paulson 2010-11-09 tidied using metis
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-06-28 haftmann 2010-06-28 tuned theory text
2010-06-02 haftmann 2010-06-02 absolute import -- must work with Main.thy / HOL-Proofs
2010-03-08 haftmann 2010-03-08 transfer: avoid camel case
2009-12-04 nipkow 2009-12-04 removed redundant lemma
2009-11-16 webertj 2009-11-16 Fixed a typo in a comment.
2009-09-01 haftmann 2009-09-01 some reorganization of number theory