| Mon, 19 Apr 2010 19:41:15 +0200 | blanchet | don't redo an axiom selection in the first round of Sledgehammer "minimize"!; | changeset | files |
| Mon, 19 Apr 2010 18:44:12 +0200 | blanchet | get rid of "conjecture_pos", which is no longer necessary now that it's Metis's job, not Sledgehammer's, to report inconsistent contexts | changeset | files |
| Mon, 19 Apr 2010 18:14:45 +0200 | blanchet | added warning about inconsistent context to Metis; | changeset | files |
| Mon, 19 Apr 2010 17:18:21 +0200 | blanchet | workaround for Proof General's off-by-a-few sendback display bug, whereby "pr" in "proof" is not highlighted | changeset | files |
| Mon, 19 Apr 2010 16:33:48 +0200 | blanchet | got rid of somewhat pointless "pairname" function in Sledgehammer | changeset | files |
| Mon, 19 Apr 2010 16:33:20 +0200 | blanchet | make Sledgehammer's "add:" and "del:" syntax really work (I hope), by comparing CNF theorems with CNF theorems | changeset | files |
| Mon, 19 Apr 2010 16:29:52 +0200 | blanchet | cosmetics | changeset | files |