clarified toplevel_error: absorb and print interrupts; tuned;

more explicit error;

tuned message;

removed unused YXML_Find_Theorems and Legacy_XML_Syntax;

more robust read_query; avoid pointless position, which is always line 1 for single-line input;

removed commented out declaration

tuned

merged

eliminate \<twosuperior> as well;

more strict identifier syntax: disallow superscripts, which tend to be used in notation such as \<^sup>\<omega>;

prefer plain subscript for identifiers;

proper low-level comparison -- heed warning by Scala compiler;

merged

prefer Code.abort with explicit error message

avoid re-inventing transitive closure

merged

theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map

tuned

tuned tactic;

abort execution of generated code with explicit exception message

merged

dockable window for Sledgehammer, based on asynchronous/parallel query operation;

tuned imports;

snippet for instr type

filter function on streams

tuned

tuned proofs;

tuned proofs;

maintain commands together with index -- avoid redundant reconstruction of full_index;

more elementary list structures for markup tree traversal;

tuning

enrich exported ML function's signature

merged

more NEWS and CONTRIBUTORS;

some documentation for adhoc overloading; spell-checked;

added examples of adhoc overloading

use uniform spelling of "adhoc"

tuned formatting of error message

tuned proofs;

tuned signature; tuned;

more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;

tuned;

tuned signature;

enabled key event to apply query;

prefer single-line HistoryTextField;

contract equalities in transfer and transfer domain rules when they are registered

expand equalities in the transfer relation in transfer_prover if the relation doesn't follow the functional structure

merged

misc tuning and simplification;

more generic button;

support for query operations that consist of parallel segments;

more tooltips;

tuned -- more explicit type Status.Value;

more explicit status for query operation; avoid output with outdated snapshot; animation rate according to status; added PIDE.document_snapshot convenience -- independent of availability of physical buffer;

tuned signature;

query process animation;

tuned signature;

tuning

tuning

tuning

tuning

export ML function (for primcorec)

more central Pretty_Tooltip.dismissed_all -- avoid spurious crash of Rich_Text_Area.robust_body in asynchronous mouse_motion_listener;

tuned proofs;