| 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 |