src/HOL/ex/Simproc_Tests.thy
2012-03-25 ago merged fork with new numeral representation (see NEWS)
2012-01-17 ago factor-cancellation simprocs now call the full simplifier to prove that factors are non-zero
2011-11-16 ago rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
2011-11-11 ago abel_cancel.ML: avoid canceling zeros, which would cause the simproc to return a trivial rewrite;
2011-11-11 ago use simproc_setup for the remaining nat_numeral simprocs
2011-11-11 ago use simproc_setup for more nat_numeral simprocs; add simproc tests
2011-11-09 ago tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
2011-11-09 ago use simproc_setup for some nat_numeral simprocs; add simproc tests
2011-11-09 ago add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
2011-10-28 ago ex/Simproc_Tests.thy: remove duplicate simprocs
2011-10-28 ago use simproc_setup for cancellation simprocs, to get proper name bindings
2011-10-27 ago 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 ago add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML