src/HOL/Number_Theory/Factorial_Ring.thy
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-09-18 haftmann 2016-09-18 more generic algebraic lemmas
2016-09-19 fleury 2016-09-19 # after multiset intersection and union symbol
2016-09-16 haftmann 2016-09-16 prefer abbreviation for trivial set conversion
2016-09-16 haftmann 2016-09-16 more lemmas
2016-09-09 nipkow 2016-09-09 msetsum -> set_mset, msetprod -> prod_mset
2016-09-05 fleury 2016-09-05 add_mset constructor in multisets
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