src/HOL/Number_Theory/Residues.thy
2016-07-09 haftmann 2016-07-09 more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat * * * more rules for setsum, setprod on intervals
2016-05-26 wenzelm 2016-05-26 isabelle update_cartouches -c -t;
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 tuned;
2015-06-19 wenzelm 2015-06-19 tuned proofs;
2015-06-19 wenzelm 2015-06-19 isabelle update_cartouches;
2015-03-16 paulson 2015-03-16 The factorial function, "fact", now has type "nat => 'a"
2015-03-10 paulson 2015-03-10 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-02-06 paulson 2014-02-06 tidied
2014-02-03 paulson 2014-02-03 fixed indentation
2014-02-02 paulson 2014-02-02 new lemmas involving phi from Lehmer AFP entry
2014-02-02 paulson 2014-02-02 Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
2014-02-01 paulson 2014-02-01 version of Fermat's Theorem for type nat
2014-01-30 haftmann 2014-01-30 more direct simplification rules for 1 div/mod numeral; added simplification rules for (- 1) div/mod numeral
2014-01-29 paulson 2014-01-29 minor adjustments
2013-11-29 traytel 2013-11-29 set_comprehension_pointfree simproc causes to many surprises if enabled by default
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2012-11-08 bulwahn 2012-11-08 adjusting proofs as the set_comprehension_pointfree simproc breaks some existing proofs
2012-03-27 huffman 2012-03-27 remove redundant lemma
2011-09-10 wenzelm 2011-09-10 misc tuning;
2011-03-13 wenzelm 2011-03-13 tuned headers;
2011-01-13 wenzelm 2011-01-13 eliminated global prems; tuned proofs;
2010-04-26 haftmann 2010-04-26 dropped group_simps, ring_simps, field_eq_simps
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2009-09-01 haftmann 2009-09-01 some reorganization of number theory