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;

slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;

remove overlay after result has arrived -- one-shot query operation;

more message markup, provided by prover;

tuned signature -- more uniform treatment of overlays as command mapping;

commands with overlay remain visible, to avoid loosing printed output;

initial update of nodes_required, for proper GUI state;

tuned signature;

avoid repeated PIDE.flush_buffers when manipulating overlays;

tuned proofs;

merged

some actual find_theorems functionality;

more general Output.result: allow to update arbitrary properties; clarified kind/instance of overlay GUI component, with separate output (subject to version as main Output);

prefer canonical order, to avoid potential fluctuation due to front-end edits;

tuned signature;

minimal print function "find_theorems", which merely echos its arguments;

support print functions with explicit arguments, as provided by overlays;

maintain overlays within node perspective; tuned signature;

some tracking of command location; tuned;

tuned proofs;

dockable window for "find" dialog (GUI only);

tuned;

more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)

more (co)datatype docs

tuned exercises

more (co)datatype documentation

more (co)datatype documentation

store relator induction in fp_result

merged

optional static analysis for Poly/ML 5.5.x;

exception trace for Poly/ML 5.5.1, using regular Isabelle output;

recode utf8 for ML, as done in feeder.pl;

more explicit read-only non-TTY mode;

clarified options;

specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;

tuned;

test recent polyml-svn, which is becoming polyml-5.5.1;

minor doc fixes

more (co)datatype docs

more (co)datatype documentation

merged

removed duplicate lemma

more (co)datatype documentation

tuning

more (co)datatype docs

tuned proof;

recovered "\<phi>\<^isub>i" from 0b02aaf7c7c5;

proper border (again) -- avoid NPE on Windows; uniform non-opaqueness -- relevant for Windows L&F;

NEWS;

added home-made tooltips; tuned signature;