move auxiliary lemma to top

add countable compacteness; replace finite_range_imp_infinite_repeats by pigeonhole_infinite

group compactness-eq-seq-compactness lemmas together

replace convergent_imp_cauchy by LIMSEQ_imp_Cauchy

tuned

removed subseq_bigger (replaced by seq_suble)

countablility of finite subsets and rational numbers

generalize compact_path_image to topological_space

re-generated components.sha1;

merged

more system-independent order of components.sha1 to keep changes monotonic;

clarified Future.error_msg: slightly more robust id check, actually suppress displaced messages;

delay to give users a chance to see what was happening, even with auto_close enabled;

updated docs

updated component again, as there was an issue with hard-coded paths in "runepar.pl"

added E-Par support

updated E component

tweaked defaults

changed type of preplay time; tuned preplaying

move preplaying to own structure

register SHA1 for Haskabelle-2013 component

register Haskabelle as a component

merged

tuned proofs;

tuned proofs;

tuned signature;

proper runtime position (cf. fe4714886d92 and Toplevel.error_msg) -- to make error messages actually appear in the document;

close tooltip after Active.action, to make it look more interactive (notably due to lack of dynamic update);

identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;

eliminated dead code;