summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files | gz |
help

(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

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;