make sure that all facts are passed to ATP from minimizer

more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"

specify timeout for "sledgehammer_tac"

tuning

Quotient Package: add mem_rsp, mem_prs, tune proofs.

merged

declare euclidean_simps [simp] at the point they are proved; avoid duplicate rule warnings;

merged

merged

avoid warnings

comment out dead code to avoid compiler warnings

legacy theorem names

remove duplicate lemma

fixed "hBOOL" of existential variables, and generate more helpers

don't select facts when using sledgehammer_tac for reconstruction

don't perform a triviality check if the goal is skipped anyway

optional reconstructor

misc tuning and simplification;

tuned pri: prefer purging of canceled execution;

tuned Document.node: maintain "touched" flag to indicate changes in entries etc.;

clarified Document.Node.clear -- retain header (cf. ML version);

clarified norm_header/header_edit -- disallow update of loaded theories;

misc tuning and simplification;

ignore irrelevant timings;

print state only for visible command, to avoid wasting resources for the larger part of the text;

early filtering of unchanged perspective;

more reliable update_perspective handler based on actual text visibility (e.g. on startup or when resizing without scrolling);

update_perspective without actual edits, bypassing the full state assignment protocol; edit_nodes/Perspective: do not touch_descendants here; propagate editor scroll events via update_perspective; misc tuning;

tuned;

handle potentially more approriate BufferUpdate.LOADED event;