src/HOL/Numeral_Simprocs.thy
2015-03-31 haftmann 2015-03-31 given up separate type classes demanding `inverse 0 = 0`
2015-03-20 paulson 2015-03-20 fixed crash in cancel_numeral_simprocs. NB they still don't work except for type nat!
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-02-10 nipkow 2014-02-10 improved lin.arith. for terms involving division
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-11-04 haftmann 2013-11-04 streamlined setup of linear arithmetic
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-04-01 huffman 2012-04-01 removed Nat_Numeral.thy, moving all theorems elsewhere
2012-03-27 huffman 2012-03-27 generalize some theorems about div/mod
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-11-11 huffman 2011-11-11 use simproc_setup for the remaining nat_numeral simprocs
2011-11-11 huffman 2011-11-11 use simproc_setup for more nat_numeral simprocs; add simproc tests
2011-11-09 huffman 2011-11-09 use simproc_setup for some nat_numeral simprocs; add simproc tests
2011-11-09 huffman 2011-11-09 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type s not in this class); test simprocs using most general type classes instead of just int and rat.
2011-10-30 huffman 2011-10-30 extend cancellation simproc patterns to cover terms like '- (2 * pi) < pi'
2011-10-28 huffman 2011-10-28 more accurate class constraints on cancellation simproc patterns
2011-10-28 huffman 2011-10-28 use simproc_setup for cancellation simprocs, to get proper name bindings
2010-07-19 haftmann 2010-07-19 tuned whitespace
2009-10-30 haftmann 2009-10-30 dedicated theory for loading numeral simprocs