[isabelle-dev] NEWS: enabled MaSh by default

[Jasmin Christian Blanchette]

    - MaSh and MeSh are now used by default together with the traditional
      MePo (Meng-Paulson) relevance filter. To disable MaSh, set the "MaSh"
      system option in Plugin Options / Isabelle / General to "none". Other
      allowed values include "sml" (for the default SML engine) and "py"
      (for the old Python engine).

This refers to Isabelle/fd539459a112.

Older NEWS made this possible:

    - New SML-based learning engines eliminate the dependency on Python
      and increase performance and reliability.

Some users have been using MaSh for quite some time now, and with the  ML implementation, due to Cezary Kaliszyk, the residual technical issues should be all gone.

To actually see MaSh in action, you can try calling Sledgehammer with the verbose option, e.g. "sledgehammer [verbose]". You should then see three lists of fact (MePo, MaSh, MeSh). If you enable spying (by setting "export SLEDGEHAMMER_SPY=yes" in "~/.isabelle/etc/settings", and why not "export NITPICK_SPY=yes" while at it), you will be locally collecting data about MaSh vs. MePo that might one day be useful for data-mining.

IMPORTANT: Please let me know quickly if you run into any technical issues connected to this. As much as I would like to have MaSh enabled in the release version (thereby increasing Sledgehammer's success rate quite a bit), we should tread carefully and disable it by default if any serious issues arise until the release.

Jasmin