| 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 | file | diff | annotate |
| Fri, 28 Oct 2011 10:33:23 +0200 | huffman | ex/Simproc_Tests.thy: remove duplicate simprocs | file | diff | annotate |
| Fri, 28 Oct 2011 11:02:27 +0200 | huffman | use simproc_setup for cancellation simprocs, to get proper name bindings | file | diff | annotate |
| 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 | file | diff | annotate |
| Fri, 21 Oct 2011 08:42:11 +0200 | huffman | add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML | file | diff | annotate |