src/HOL/Number_Theory/Gauss.thy
19 months ago haftmann 2017-10-08 euclidean rings need no normalization
2017-04-07 wenzelm 2017-04-07 tuned headers;
2017-04-06 wenzelm 2017-04-06 misc tuning and modernization;
2016-12-21 haftmann 2016-12-21 removed dangerous simp rule: prime computations can be excessively long
2016-10-17 eberlm 2016-10-17 Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
2016-10-17 nipkow 2016-10-17 setprod -> prod
2016-10-16 haftmann 2016-10-16 more standardized names
2016-08-08 eberlm 2016-08-08 is_prime -> prime
2016-07-29 wenzelm 2016-07-29 more accurate cong del; tuned proofs;
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 dropped various legacy fact bindings
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-02-19 haftmann 2015-02-19 more canonical order of subscriptions avoids superfluous facts
2015-02-15 haftmann 2015-02-15 explicit equivalence for strict order on lattices
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-10-09 haftmann 2014-10-09 more foundational definition for predicate even
2014-09-21 haftmann 2014-09-21 explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
2014-09-09 blanchet 2014-09-09 avoid internal fact
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-06-28 haftmann 2014-06-28 fact consolidation
2014-04-12 nipkow 2014-04-12 made mult_pos_pos a simp rule
2014-02-24 paulson 2014-02-24 Gauss.thy ported from Old_Number_Theory (unfinished)