src/HOL/Number_Theory/Factorial_Ring.thy
2016-08-08 eberlm 2016-08-08 is_prime -> prime
2016-07-25 wenzelm 2016-07-25 merged
2016-07-22 wenzelm 2016-07-22 tuned proofs -- avoid improper use of "this";
2016-07-22 eberlm 2016-07-22 Removed redundant material related to primes
2016-07-21 eberlm 2016-07-21 Overhaul of prime/multiplicity/prime_factors
2016-07-13 eberlm 2016-07-13 Reformed factorial rings
2016-05-24 eberlm 2016-05-24 Backed out changeset 8230358fab88
2016-05-24 eberlm 2016-05-24 Deleted problematic code equation in Codegenerator_Test
2016-04-26 wenzelm 2016-04-26 some uses of 'obtain' with structure statement;
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-03-03 haftmann 2016-03-03 constructive formulation of factorization
2016-02-18 haftmann 2016-02-18 more theorems
2016-02-17 haftmann 2016-02-17 dropped various legacy fact bindings
2015-07-27 haftmann 2015-07-27 formal class for factorial (semi)rings