refactor large ML file

use Local_Theory.define instead of Specification.definition for internal constants

compile

renamed many Sledgehammer ML files to clarify structure

renamed ML file

tuned comment

tuned ML file name

tuned ML file name

less hermetic tactics

merged

reverted unsound optimization

got rid of one of two Metis variants

tuning

unskolemize SPASS formula to ensure that the variables are in the right order for 'metis's skolemizer

killed needless pass

dependency reporting for code generation errors

more abstract dictionary construction

reduced prominence of "permissive code generation"

split rules for of_bool, similar to if

don't forget the last inference(s) after conjecture skolemization

centralized & repaired handling of bound variables in intermediate data structure (viva de Bruijn)

keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized

renamed Sledgehammer options for symmetry between positive and negative versions

more robust w.r.t. exceptions raised by proof methods

tuning

compile

tuning

added 'algebra' and 'meson' to 'try0'

made 'try0' (more) silent

'using' already uses the new Skolemizer, enabling a subtly shorter syntax

merged

extended cardinals library