handle Skolems gracefully for SPASS as well

move some Z3 specifics out (and into private repository with the rest of the Z3-specific code)

reverse Skolem function arguments

correcly recognize E skolemization steps that are wrapped in a 'shift_quantors' inference

fixed confusion between 'prop' and 'bool' introduced in 4960647932ec

generalize method list further to list of list (clustering preferred methods together)

store alternative proof methods in Isar data structure

tuning

added 'meson' to the mix

tuning

made SML/NJ happy

use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning

generate proper succedent for cases with trivial branches

tuning

simplify generated propositions

use 'prop' rather than 'bool' systematically in Isar reconstruction code

tuning

use 'arith' when appropriate in Z3 proofs

robustness in degenerate case + tuning

use simplifier for rewrite

more aggressive merging

implemented Z3 skolemization

inline Z3 hypotheses

merge

merge

merged

better handling of Z3 proof blocks

disambiguation of interpretation prefixes

more algebraic terminology for theories about big operators

more antiquotations;