tuned signature;

tuned;

unused;

tuned signature (again);

tuned;

tuned;

proper deps from build_graph, not imports_graph (amending 0c704aba71e3);

misc tuning: more direct access to ancestors, without build_graph;

tuned signature (again);

clarified signature: reduce explicit access to static Sessions.Structure;

tuned signature;

clarified modules (again);

tuned;

tuned signature;

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

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);