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

tuned comments;

handle _ should be avoided (spurious Interrupt will spoil the game);

added norm_export_morphism;

added exit_global, exit_result, exit_result_global; ProofContext.norm_export_morphism;

LocalTheory.exit_global;

HOL no longer depends on HOL-Plain;

setmp_noncritical;

join earlier promises first;

proper setmp_thread_data for nested execute (cf. join_loop);

promise_result: enforce strictly sequential dependencies, via serial numbers;

do not cvs update for doc test (switching to mercurial, update done outside once and for all)

use mercurial repository for isatest

thread_data: include thread name, export access; more tracing;

setmp_noncritical;

dequeue_towards: return bound for unfinished tasks;

moved release_results to future.ML; get_some: simplified via Future.release_results;

added release_results (formerly in par_list.ML); more informative trace_active; join_results: avoid deadlock via nested SYNCHRONOIZED, more robust active join, less rechecking of tasks;

Future.release_results;

more tracing;

Theory.checkpoint for main operations, admits concurrent proofs;

promise: include check into future body, i.e. joined results are always valid; pending future derivations: shared ref within whole theory body, i.e. end-of-theory joins *all* derivations ever forked from a version of the theory; simplified rep_deriv;