schedule_futures: save memory for non-parallel proofs, by applying after_load as soon as possible here;

future_result: avoid expensive norm_proof (consider usedir option -Q false in low-memory situations);

added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;

remove_thy: perform PureThy.cancel_proofs; schedule_futures: PureThy.join_proofs before after_load -- achieves parallel error messages;

added cancel_proofs, based on task groups of "entered" proofs;

added pending_groups -- accumulates task groups of local derivations only;

added cancel_group;

merged

schedule_futures: tuned final consolidation, explicit after_load phase;

load_thy: explicit after_load phase for presentation;

excursion: commit_exit internally -- checkpoints are fully persistent now; excursion: do not force intermediate result states yet -- great performance improvement;

slightly more robust matching of session name;

merged

fixed proof involving dvd;

tuned;

added force_result;

use_thys: perform consolidate_thy on loaded theories, which removes failed nodes in post-hoc fashion;

simplified join_proofs;

merged

added split_thy_path;

added running task markup;

tuned;

merged

merged

merged.

fix proof broken by changes in dvd theory

merged.

remove type-specific proofs

add lemma dvd_diff to class comm_ring_1

add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1

move lemmas mult_minus{left,right} inside class ring

clean up division_ring proofs

add class ring_div; generalize mod/diff/minus proofs for class ring_div

generalize zmod_zmod_cancel -> mod_mod_cancel

generalize some div/mod lemmas; remove type-specific proofs

add tracing for domain package proofs

rename abbreviation square -> power2, to match theorem names

merged

split of Imperative_HOL theories from HOL-Library

NEWS and CONTRIBUTORS

dded code_thm antiquotation

made SML/NJ happy

merged

merged

tuned siganture of locale.ML

tuned signature; internal code reorganisation

tuned signature; changed locale predicate name convention

changed locale predicate name convention

inductive: added fork_mono flag;

added fork_mono flag, which is usually enabled in batch-mode only; mono rule: unnamed LocalTheory.node ensures proper joining of pending proofs;

Proof.global_future_terminal_proof;

Proof.global_future_proof;

future_proof: refined version covers local_future_proof and global_future_proof; future_proof: refrain from full Variable.auto_fixes -- not all contexts in the stack are in body mode; refined is_relevant: mode check; added local/global_future_terminal_proof;

more robust propagation of errors through bulk jobs;

qed/after_qed: singleton result;

Proof.future_terminal_proof: no fork for interactive mode -- proofs need to be checked immediately here;

future_terminal_proof: no fork for interactive mode, assert_backward;

added local_theory';

merged

proper local_theory after Class.class

more parallel loading;

more parallel loading;

merged

merged.

make cont_proc handle eta-contracted terms

implement is_closed_term using Term.loose_bvar

use Thm.close_derivation instead of standard

tuned;

merged

renamed structure ParList to Par_List;

parallelized merge_data;

tuned map: reduced overhead due to bulk jobs; tuned join_results: reduced overhead for finished futures; tuned;

added is_valid; added extend: support bulk jobs; tuned;

future_terminal_proof: check Future.enabled;

merged

locale -> old_locale, new_locale -> locale

locale -> old_locale, new_locale -> locale

locale -> old_locale, new_locale -> locale

removed locale adaption layer

rearranged target theories

removed locale adaption layer

merged

misc tuning and modernization;

merged.

add lemma psize_unique; simplify some proofs

minimize imports

parallelize some internal proofs via Proof.future_terminal_proof;

added future_terminal_proof;

Isar.init;

simplified tty model -- back to plain list history, which is independent of editor model;

added is_control, is_regular, is_theory_begin;

more precise is_relevant: requires original main goal, not initial goal state; tuned future_proof: minimal modification of goal state, retain original maxidx; tuned;

tuned protect, conclude: Drule.comp_no_flatten;

added comp_no_flatten;

future proofs: back to Future.fork_pri ~1 for improved parallelism;

cancel: unique threads;

more reactive scheduler: reduced loop timeout, propagate broadcast interrupt via TaskQueue.cancel_all;

added eq_group; opaque signature match prevents accidental task/group equality; added cancel_all;

merged

separator, is_qualified

added instance for bot, top

added binding.ML

merged

merged

improved boostrap order: theory_target.ML before expression.ML

named code theorem for Fract_norm

tuned settings;

merged

removed references to OldTerm.*

tuned message_text;

removed obsolete XML mode; tuned comments; tuned;

xsymbols: use plain Symbol.output; explicit rendering of message body: print mode is always YXML, markup is only observed for singleton text (avoids overlap of inner tokens with certain status messages), test XML markup is outermost (allows Proof General font-lock); Markup.no_output;

Markup.no_output;

added output; improved encode_raw: map empty to empty; tuned;

removed unused add_substring; back to simple list implementation;

renamed syntax constant "_var" to "_variable", to avoid clash with internal token marker;

removed print mode "PGASCII" -- 7-bit ASCII communication now always enabled;

updated rendering of inner token markup;

more detailed inner token markup;

added numeral, which supercedes num, xnum, float; renamed xstr to inner_string;