convenience

name tuning

learning should honor the fact override and the chained facts

fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully

MaSh docs

added "learn_from_atp" command to MaSh, for patient users

get rid of redundant "xxx_INSTALLED" environment variabl

add versioning to MaSh state + cleanup dead code

eliminated special handling of init case, now that "mash.py" has been optimized to handle sequences of add gracefully

more MaSh docs

mention MaSh in docs

use good old MePo filter for SMT solvers by default, since arithmetic is built-in for them

added locality as a MaSh feature

learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds

learn command in MaSh

added possibility of running external MaSh commands asynchronously

renamed ML structures

renamed ML files

renamed "iter" fact filter to "MePo" (Meng--Paulson)

handle local facts smoothly in MaSh

fixed explosion when computing accessibility

use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)

tuning

merged

further imitation of "usedir" shell script; Pure/build observes build_images option, unlike traditional version; tuned signature;

make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests

export code relatively to master directory

require explicit initialization of options; more explicit Position operations;

tuned signature;

define build_options from command line;