src/HOL/ex/Simproc_Tests.thy
Fri, 11 Nov 2011 11:30:31 +0100 huffman use simproc_setup for the remaining nat_numeral simprocs
Fri, 11 Nov 2011 11:11:03 +0100 huffman use simproc_setup for more nat_numeral simprocs; add simproc tests
Wed, 09 Nov 2011 15:33:24 +0100 huffman tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
Wed, 09 Nov 2011 11:44:42 +0100 huffman use simproc_setup for some nat_numeral simprocs; add simproc tests
Wed, 09 Nov 2011 10:58:08 +0100 huffman add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
Fri, 28 Oct 2011 10:33:23 +0200 huffman ex/Simproc_Tests.thy: remove duplicate simprocs
Fri, 28 Oct 2011 11:02:27 +0200 huffman use simproc_setup for cancellation simprocs, to get proper name bindings
Thu, 27 Oct 2011 07:46:57 +0200 huffman 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
Fri, 21 Oct 2011 08:42:11 +0200 huffman add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
less more (0) tip