2015-08-08 haftmann 2015-08-08 direct bootstrap of integer division from natural division
2015-03-31 haftmann 2015-03-31 given up separate type classes demanding `inverse 0 = 0`
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2012-07-27 huffman 2012-07-27 give Nat_Arith simprocs proper name bindings by using simproc_setup
2012-07-27 huffman 2012-07-27 replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
2012-07-20 huffman 2012-07-20 make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-01-17 huffman 2012-01-17 factor-cancellation simprocs now call the full simplifier to prove that factors are non-zero
2011-11-16 huffman 2011-11-16 rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
2011-11-11 huffman 2011-11-11 abel_cancel.ML: avoid canceling zeros, which would cause the simproc to return a trivial rewrite; add tests for abel_cancel simprocs
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 tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
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-28 huffman 2011-10-28 ex/Simproc_Tests.thy: remove duplicate simprocs
2011-10-28 huffman 2011-10-28 use simproc_setup for cancellation simprocs, to get proper name bindings
2011-10-27 huffman 2011-10-27 fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left
2011-10-21 huffman 2011-10-21 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML