| Mon, 21 May 2012 11:31:52 +0200 | blanchet | include "ext" in all Satallax proofs | changeset | files |
| Mon, 21 May 2012 10:39:32 +0200 | blanchet | add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis" | changeset | files |
| Mon, 21 May 2012 10:39:31 +0200 | blanchet | tuning | changeset | files |
| Mon, 21 May 2012 10:39:31 +0200 | blanchet | added helper -- cf. SET616^5 | changeset | files |
| Fri, 18 May 2012 17:36:20 +0200 | kuncar | note Quotient theorem for typedefs in setup_lifting | changeset | files |
| Fri, 18 May 2012 16:43:38 +0200 | blanchet | added a timeout to "try0" in Mirabelle | changeset | files |
| Fri, 18 May 2012 15:08:08 +0200 | kuncar | don't generate code in Word because it breaks the current code setup | changeset | files |
| Thu, 17 May 2012 13:36:23 +0200 | blanchet | robustly parse Z3 4.0's output (with outcome appearing on first rather than last line) | changeset | files |