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

Fixed a presentation error

Importation of basic group theory results, due to Jakob von Raumer from his AFP entry Jordan-Hölder Theorem

tuned whitespace;

tuned;

clarified signature, although "sql" argument is de-facto mandatory;

tuned;

proper SQL (amending 7ab9bac1ca96);

clarified signature: more explicit "synchronized" regions;

more robust interrupt handling, notably for Build_Job.terminate();

clarified signature: works for general Build_Job;

tuned;

clarified modules;

clarified signature;

proper log_lines, without protocol messages (amending cb3f5361fbca);

clarified signature;

tuned messages;