src/HOL/Number_Theory/Eratosthenes.thy
2016-08-08 eberlm 2016-08-08 is_prime -> prime
2016-07-21 eberlm 2016-07-21 Overhaul of prime/multiplicity/prime_factors
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-02-17 haftmann 2016-02-17 cleansed junk-producing interpretations for gcd/lcm on nat altogether
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-09-13 wenzelm 2015-09-13 renamed method "goals" to "goal_cases" to emphasize its meaning;
2015-06-26 wenzelm 2015-06-26 tuned proofs;
2015-06-19 wenzelm 2015-06-19 tuned proofs;
2015-06-19 wenzelm 2015-06-19 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-12 haftmann 2014-10-12 generalized and consolidated some theorems concerning divisibility
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-01-24 paulson 2014-01-24 Restored Suc rather than +1, and using Library/Binimial
2013-10-31 haftmann 2013-10-31 generalised lemma
2013-06-15 haftmann 2013-06-15 selection operator smallest_prime_beyond
2013-02-17 haftmann 2013-02-17 Sieve of Eratosthenes