src/HOL/Number_Theory/Gauss.thy
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)