merged

avoid hardwired frees; tuned;

added Thm.forall_intr_name;

added 'proposition' command;

fewer aliases for toplevel theorem statements;

just one theorem kind, which is legacy anyway;

pretty_const: proper local name space; tuned;

collect the names from goals in favor of fragile exports

compile

tuning

avoid legacy syntax

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

added "!=" (disequality) as a TPTP binary operator, since it pops up in LEO-II proofs

merged

tuned signature;

produce nodes_status outside GUI thread, to avoid a few milliseconds of blocking;

avoid too aggressive optimization of 'finite' predicate

avoid unsound simplification of (C (s x)) when s is a selector but not C's

extended theory exporter to also export MePo-selected facts

speed up MaSh duplicate check

sped up MaSh nickname generation

merged

more explicit umask for important directories: e.g. relevant for Windows 10, where implicit g=rwx leads to odd failure of chmod -w for heap images;

speed up MaSh

updated docs and NEWS

updated docs

removed Nitpick nonblocking mode, that was never really used

adapted example