unit_source: more rigid parsing, stop after final qed;

excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context; tuned;

replaced can_defer by is_relevant (negation); future_proof: declare forked goal to prevent accidental generalization (e.g. instance goal);

datatype transition: internal trans field is maintained in reverse order; tuned;

future_proof: protect conclusion of deferred proof state;

future_schedule: back to one group for all loader tasks;

tuned comments;

fixed

renamed promise to future, tuned related interfaces;

more robust treatment of Interrupt (cf. exn.ML); future_schedule: group each theory separately;

more robust treatment of Interrupt; added release_all, release_first; proper signature;

more robust treatment of Interrupt (cf. exn.ML);

removed release_results (cf. Exn.release_all, Exn.release_first);

more precise join_futures, improved termination;

added more_antiquote.ML

extract Isabelle dist name correctly

unit_source: explicit treatment of 'oops' proofs;

promise_proof: proper statement with empty vars;

load_thy: more precise treatment of improper cmd or proof (notably 'oops');

schedule_tasks: single theory is loaded concurrently as well (cf. concurrent Toplevel.excursion);

added unit_source: commands with proof;

begin_proof: avoid race condition wrt. skip_proofs flag; replaced command_excursion by excursion, which is based on units of command/proof pairs; excursion: basic support for proof promises;

load_thy: Toplevel.excursion based on units of command/proof pairs;

more command categories; tuned;

renamed Future.fork_irrelevant to Future.fork_background; tuned;

export explicit joint_futures, removed Theory.at_end hook; renamed Future.fork_irrelevant to Future.fork_background;

tuned

turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);

Toplevel.commit_exit: position;

export setmp_thread_position; commit_exit: position; added plain command execution; simplified command_excursion, eliminated old (present_)excursion;

simplified process_file, eliminated Toplevel.excursion; load_thy: separation of Toplevel.command_excursion and ThyOutput.present_thy (intermediate state persist until commit_exit);

clarified codegen interfaces

tuned

reorganized examples

fixed slips

re-canibalised manual

slightly different command line for makedist_mercurial

put_thms: ContextPosition.set_visible false;

added type pp, which helps installing polymorphic pretty printers;

added str_of;

install_pp Future.T (polyml only);

report_token/parse_token: back to context-less version;

back to plain Position.report for regular references;

back to plain Position.report for regular references; ContextPosition.report_visible for decls; report_token/parse_token: back to context-less version;

promise global proofs;

renamed report to report_visible; tuned comments;

code example: back to individual ML commands, which are now thread-safe;

ContextPosition.report; parse_token/report_token: explicit context;

target update: invisible context position avoids duplication of reports etc.;

Context position visibility.

added context_position.ML;

more precise redundancy check

clarified dependencies between arith tools

separate HOL-Main image

polished code generator setup

added theory antiquotation