tweaked 'clone' formula detection

fine-tuned Isar reconstruction, esp. boolean simplifications

centralized boolean simplification so that e.g. LEO-II benefits from it

careful when compressing 'obtains'

better handling of variable names

try to get rid of skolems first

nicer generated variable names

tuning

tuning

no need to 'obtain' variables not in formula

more precise handling of LEO-II skolemization

beware of 'skolem' rules that do not skolemize (e.g. LEO-II)

tuning

peek instead of joining -- is perhaps less risky

export ML function

compile

removed 'metisFT' support in Mirabelle

removed Mirabelle minimization code

modernized Mirabelle (a bit) and made it compile

restored a bit of laziness

reorder quantifiers to ease Z3 skolemization

tuned order of arguments

tuned name context code

tuned whitespace

more rational unskolemizing of names

added appropriate method for skolemization of Z3 steps to the mix

pushing skolems under 'iff' sometimes breaks things further down the proof (as was to be feared)

honor 'try0' also for one-liners

tentatively took out 'fastforce' from the set of tried methods -- it seems to be largely subsumed and is hard to silence

further minimize one-liner