mark hard tabs as single chunks, as required by jEdit;

updated READMEs;

property "tooltip-dismiss-delay" is edited in ms, not seconds; explicit tooltip_dismiss_delay boundaries for further robustness;

moved XML/YXML to src/Pure/PIDE; tuned comments;

pass raw messages through xml_cache actor, which is important to retain ordering of results (e.g. read_command reports before assign, cf. 383c9d758a56);

pseudo-definition for perms on sets; tuned

remove duplicate lemma nat_zero in favor of nat_0

merged

merged

modify nominal packages to better respect set/pred distinction

merged

remove unused assumption from lemma posreal_complete

tuned specifications

merged

tuned proof

merged

assert Pure equations for theorem references; avoid dynamic reference to fact

assert Pure equations for theorem references; tuned

tuned specifications and proofs

merged

remove duplicate lemma finite_choice in favor of finite_set_choice

simplify proof

shorten some proofs

remove redundant simp rules ceiling_floor and floor_ceiling

misc tuning and simplification of proofs;

Document.removed_versions on Scala side;

discontinued predefined empty command (obsolete!?);

discontinued global execs: store exec value directly within entries; simplified entries: no extra copy of command_id;

Document.remove_versions on ML side;

some support to prune_history; clarified signature: recent_stable is supposed to be always defined;