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;

special treatment of structure index 1 in Pure, including legacy warning;

compile

added "max_calls" option to get a fixed number of Sledgehammer calls per theory

beef up "sledgehammer_tac" reconstructor

clean up Sledgehammer tactic

fixed document;