| Thu, 10 May 2012 16:56:23 +0200 | blanchet | distinguish between instantiated and uninstantiated inductions -- the latter are OK for first-order provers | changeset | files |
| Thu, 10 May 2012 12:23:20 +0200 | huffman | temporarily comment out broken nitpick example | changeset | files |
| Thu, 10 May 2012 09:10:43 +0200 | huffman | convert real number theory to use lifting/transfer | changeset | files |
| Mon, 07 May 2012 15:04:17 +0200 | huffman | tuned ordering of lemmas | changeset | files |
| Thu, 10 May 2012 10:07:41 +0200 | blanchet | pass fewer facts to LEO-II and Satallax | changeset | files |
| Thu, 10 May 2012 10:07:40 +0200 | blanchet | tweak LEO-II setup | changeset | files |
| Thu, 10 May 2012 10:07:40 +0200 | blanchet | use raw monomorphic encoding with Waldmeister, to avoid overloading it with too many function symbols (as would be the case using mangled monomorphic encodings) | changeset | files |