put annotate in own structure

support assumptions as facts for preplaying

some minor improvements in shrink_proof

some support for ML runtime statistics;

prefer tight Markup.print_int/parse_int for property values;

clarified new identifier syntax: exclude \<^isup>, include subscripted prime (to allow imitating full identifier here);

eliminated slightly odd identifiers;

tuned syntax, potentially more robust;

smarter list layout;

repaired text following 491c5c81c2e8;

merged

introduce filter_lim as a generatlization of tendsto

merged

based countable topological basis on Countable_Set

qualified interpretation of sigma_algebra, to avoid name clashes

eliminated finite_set_sequence with countable set

support for sub-structured identifier syntax (inactive);

eliminated some improper identifiers;

add upper bounds for factorial and binomial; add equation for binomial using nat-division (both from AFP/Girth_Chromatic)

tuned signature; tuned;

more uniform Symbol.is_ascii_identifier in ML/Scala;

tuned;

clarified Symbol.scan_ascii_id; ATP: follow change from Symbol.scan_id to Symbol.scan_ascii_id, assuming that this was meant here, not fully symbolic Isabelle identifiers;

tuned;

convenience operations for table as set;

removed remains of Oheimb's double-space (cf. 0a5af667dc75);

tuned;

merged

updated two components

simplify code slightly

avoid non-ASCII sign

generate a parameterized correspondence relation

quot_thm_crel

add option_fold

add binomial_ge_n_over_k_pow_k

removed tool that was never finished

added file headers

updated MaSh doc

moved MaSh's Python code into Isabelle

updated NEWS etc.

distinguish declated tfrees from other tfrees -- only the later can be optimized away

clarified status of Legacy_XML_Syntax, despite lack of Proofterm_XML;

reset active areas on content update;

more general sendback properties; support for padding of line boundary, e.g. for ad-hoc insertion of commands via 'help';

tuned command descriptions;

refined outer syntax 'help' command;

tuned signature;

always reset active areas;

no special treatment of control_reset, in accordance to other control styles;

tuned signature;

tuned signature;

tuned signature;

tuned signature; uniform view.fontsize fallback;

renamed main plugin object to PIDE;

tuned signature -- avoid intrusion of module Path in generic PIDE concepts;

explicit module UTF8;