merged

clarified priority of "skipped" proofs, which might take long but do not produce relevant information (potential conflict of quick interactive feedback vs. performance in batch mode);

simplified / clarified execution priority: auto prints << 0, proofs < 0, eval = 0, print_state = 1;

paint unassigned/unchanged nodes as unprocessed -- relevant for editor_continuous_checking = false;

allow explicit indication of required node: full eval, no prints;

simplified flag for continuous checking: avoid GUI complexity and slow checking of all theories (including prints);

more work on (co)datatype docs

more (co)datatype documentation

merged

tuned proofs;

more uniform border;

proper PIDE markup for codegen arguments;

less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace; propagate flush from ML to Scala via special protocol message; more formal type Message_Channel.message;

tuned -- more uniform ML vs. Scala;

recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;

more timing;

more timing; tuned -- Execution.is_running always holds due to immediate start;

removed spurious headings

more (co)datatype documentation

avoid DUP error in local context

sketched documentation for new (co)datatype package

tuned docs (the function package isn't so new anymore)

tuned comments;

tuned;

type theory is purely value-oriented;

pro-forma Execution.reset, despite lack of final join/commit;

tuned signature; removed notoriously outdated comments;

tuned;

de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;

merged

tuned intro

silenced subsumption warnings for default code equations entirely

merged

NEWS; tuned description;

tuned proofs;

updated key bindings to execution range;

traverse node on change of "required" state;

keep memo_exec execution running, which is important to cancel goal forks eventually; run as nested worker task to keep main group valid, even after cancelation of removed subgroups; do not memoize interrupt, but absorb it silently in main execution; Goal.purge_futures: rough sanity check of group status;

maintain explicit execution frontier: avoid conflict with former task via static dependency; start execution immediate after assignment, to keep frontier simple;

afford higher execution priority by default: defer proofs and thus stretch parallelism over whole document;

clarified conditions for node traversal;

tuned;

pro-forma Goal.reset_futures, despite lack of final join/commit;

tuned;

tuned;

back to model.update_perspective with delay (cf. a20631db9c8a);

show displaced messages (e.g. from protocol thread) as raw output;

actually purge removed goal futures -- avoid memory leak;

tuned -- less redundant data structure;

always init GUI state;

tuned signature;

discontinued notion of "stable" result -- running execution is never canceled;

obsolete;

support declarative editor_execution_range, instead of old-style check/cancel buttons;

avoid duplicating Var when the types do not quite fit -- since this step occurs before type inference

updated Sledgehammer prover versions

parse nonnumeric identifiers in E proofs correctly

simplified Vampire hack -- no need to run it for other ATPs

added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")

prefer examples that work out of the box;

breakable @{file};

prefer existing swipl;

avoid machine running batch process for months;

more converse(p) theorems; tuned proofs;

more uniform cleanup;

tuned;

discontinued historic document formats;

avoid predefined symbols -- allow editing with Isabelle/jEdit in isabelle-news mode;

tuned;

discontinued ISABELLE_DOC_FORMAT;

more direct inclusion of tikz pictures;

obsolete;

documentation is always in PDF;

merged;

clarified Goal.stable_futures after 00170ef1dc39: running tasks are considered stable, without potentially blocking join;

clarified meaning of options for "isabelle options";

more correct context for dynamic invocations of static code conversions etc.

support isabelle options -g;

tuned spelling;

tuned;

standardized aliases;

transfer rule for {c,d}tor_{,un}fold

two useful relation theorems

factored syntactic type classes for bot and top (by Alessandro Coglio)

derive specialized version of full fixpoint induction (with admissibility)

export mono_thm

merged Def_Init_Sound_X into Def_Init_X

proper transfer rule format for map_transfer

merged

eliminate duplicate calls when moving to closed form -- graph decomposition chokes on duplicates

removed obsolete HOL-Boogie session; keep examples that also test SMT solvers, using a minimal version of the old Boogie loader

transfer stored bnf theorems into the "current" theory when retrieving a bnf (avoids non-trivial merges)

separate ML interface to note facts of a bnf

transfer rule for map (not yet registered as a transfer rule)

tuned exercises

clarified option name, with improved sort order wrt. "time" options;