src/HOL/Old_Number_Theory/WilsonRuss.thy
2015-11-17 paulson 2015-11-17 Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
2015-11-13 paulson 2015-11-13 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
2015-10-10 wenzelm 2015-10-10 isabelle update_cartouches;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
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
2012-04-02 huffman 2012-04-02 add simp rules for dvd on negative numerals
2012-03-27 huffman 2012-03-27 generalized lemma zpower_zmod
2012-03-27 huffman 2012-03-27 remove redundant lemma
2011-09-07 huffman 2011-09-07 avoid using legacy theorem names
2011-09-06 huffman 2011-09-06 avoid using legacy theorem names
2011-05-13 wenzelm 2011-05-13 proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
2010-09-06 wenzelm 2010-09-06 more antiquotations;
2010-08-06 wenzelm 2010-08-06 modernized specifications; tuned headers;
2010-03-02 krauss 2010-03-02 killed more recdefs
2010-02-08 haftmann 2010-02-08 tuned proofs
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-09-01 haftmann 2009-09-01 some reorganization of number theory