blanchet [Tue, 06 Oct 2015 09:27:31 +0200] rev 61331
avoid legacy syntax
blanchet [Mon, 05 Oct 2015 23:03:50 +0200] rev 61330
further improved fine point w.r.t. replaying in the presence of chained facts and a non-empty meta-quantifier prefix + avoid printing internal names in backquotes
blanchet [Mon, 05 Oct 2015 21:46:48 +0200] rev 61329
added "!=" (disequality) as a TPTP binary operator, since it pops up in LEO-II proofs
wenzelm [Mon, 05 Oct 2015 18:03:58 +0200] rev 61328
merged
wenzelm [Mon, 05 Oct 2015 18:03:52 +0200] rev 61327
tuned signature;
wenzelm [Mon, 05 Oct 2015 14:17:20 +0200] rev 61326
produce nodes_status outside GUI thread, to avoid a few milliseconds of blocking;
blanchet [Mon, 05 Oct 2015 16:14:33 +0200] rev 61325
avoid too aggressive optimization of 'finite' predicate
blanchet [Mon, 05 Oct 2015 15:57:25 +0200] rev 61324
avoid unsound simplification of (C (s x)) when s is a selector but not C's
blanchet [Mon, 05 Oct 2015 13:26:25 +0200] rev 61323
extended theory exporter to also export MePo-selected facts
blanchet [Sun, 04 Oct 2015 17:48:34 +0200] rev 61322
speed up MaSh duplicate check