| Thu, 01 Dec 2011 13:34:12 +0100 | blanchet | tuning | file | diff | annotate |
| Fri, 18 Nov 2011 11:47:12 +0100 | blanchet | more "metis" calls in example | file | diff | annotate |
| Thu, 17 Nov 2011 06:01:47 +0100 | huffman | Int.thy: remove duplicate lemmas double_less_0_iff and odd_less_0, use {even,odd}_less_0_iff instead | file | diff | annotate |
| Tue, 15 Nov 2011 12:49:05 +0100 | huffman | Metis_Examples/Big_O.thy: add number_ring class constraints, adapt proofs to use cancellation simprocs | 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 |
| Mon, 06 Jun 2011 20:36:35 +0200 | blanchet | tuned Metis examples | file | diff | annotate | base |