avoid premature Properties.uncompress: allow blob to be stored in another database;

more robust: synchronized access to database;

clarified signature: do not expose global state to object-oriented variants;

tuned comments and outline;

merged

Imported a theorem about Infinite_Sum. Importing this theory a bit earlier is causing syntactic ambiguities with Infinite_Set_Sum however; no_notation needed

A little bit more tidying up

tweaked Sledgehammer interaction

there won't be an E version 2.7

reverted 0506c3273814 -- the message is still useful

compile

adopt terminology suggested by Larry Paulson

more robust E proof parsing

avoid double 'Warning:' in Sledgehammer messages

tweaked abduction in Sledgehammer

slightly more documentation

renamed new Sledgehammer option

updated documentation

improve ad hoc abduction in Sledgehammer

tuning

don't apply abduction and consistency checking to goals of the form 'False'

implemented ad hoc abduction in Sledgehammer with E

tuned;

clarified scope of "serial" and "numa_index" within database;

clarified signature: allow more general init, e.g. from existing database;

clarified signature: allow to provide session_heaps by different means, e.g. from tmp directory or alternative session structure;

tuned;

simplified somewhat pointless error message (see also 0189fe0f6452);

clafified signature: simplify object-oriented reuse;

revert pointless 375c6b9ce9ea: overall thread context is already uninterruptible (see 54ac957c53ec);

tuned whitespace;

merged