blanchet [Mon, 19 Apr 2010 18:14:45 +0200] rev 36230
added warning about inconsistent context to Metis;
it makes more sense here than in Sledgehammer, because Sledgehammer is unsound and there's no point in having people panicking about the consistency of their context when their context is in fact consistent
blanchet [Mon, 19 Apr 2010 17:18:21 +0200] rev 36229
workaround for Proof General's off-by-a-few sendback display bug, whereby "pr" in "proof" is not highlighted
blanchet [Mon, 19 Apr 2010 16:33:48 +0200] rev 36228
got rid of somewhat pointless "pairname" function in Sledgehammer
blanchet [Mon, 19 Apr 2010 16:33:20 +0200] rev 36227
make Sledgehammer's "add:" and "del:" syntax really work (I hope), by comparing CNF theorems with CNF theorems
blanchet [Mon, 19 Apr 2010 16:29:52 +0200] rev 36226
cosmetics
blanchet [Mon, 19 Apr 2010 15:24:57 +0200] rev 36225
cosmetics
blanchet [Mon, 19 Apr 2010 15:21:35 +0200] rev 36224
cosmetics
blanchet [Mon, 19 Apr 2010 15:15:21 +0200] rev 36223
make Sledgehammer's minimizer also minimize Isar proofs
blanchet [Mon, 19 Apr 2010 11:54:07 +0200] rev 36222
don't use readable names if proof reconstruction is needed, because it uses the structure of names
blanchet [Mon, 19 Apr 2010 11:02:00 +0200] rev 36221
allow "_" in TPTP names in debug mode