avoid failure of "isabelle build -o skip_proofs";

merged

recovered stderr for PIDE batch-build, such as "Browser info at ...", "Document at ..." (see also 940195fbb282, 5469bacf5573, 5c4800f6b25a);

more compact command_timings, as in former batch-build;

unused;

unused --- superseded by PIDE messages;

more thorough cleanup, e.g. before ML_Heap.save;

discontinued old batch-build functionality;

tailored towards remaining essence

merged

tuned

added theory Tree23_of_List

more robust treatment of thm_names, with strict check after all theories are loaded;

a few more lemmas

merged

lemmas about sets and the enumerate operator

yet another little lemma

merged

merged

merged

strengthened a lemma

A new lemma about abstract Sum / Prod

separation of reversed bit lists from other material

merged

avoid exhaustion of worker threads, notably due to complex interaction of future/promise/lazy in Proofterm.make_thm_node;

more robust: insist in finished future;

unused;

further refinement of code equations for mask operation

uniform mask operation

clearer separation of pre-word bit list material

added lemma

more consequent transferability

more robust scheduler shutdown, notably for spurious crashes;

unclear why I ever asked for type tree2

enforce pide_session to see if all isabelle_cronjob tasks work smoothly with it;

proper pretty printing for latex output, notably for pide_session=true (default);

clarified name to avoid duplication (no distinction of data on host = lrzcloud2);

clarified names;

more errors;

follow Phabricator update 2020 Week 27;

tuned;

unused;

clarified errors: avoid hiding of import_errors/dir_errors by their consequences (file-access problems);

clarified errors: avoid accidental import from other session that happens to be within overall selection (notably "isabelle build -a");

clarified signature;

clarified order --- proper sorting of requirements;

obsolete (see 9cde8c4ea5a5);

tuned --- based on hints by IntelliJ;

tuned signature;

updated to polyml-5.8.1 (official release);

subtle change of Theory_Data extend/merge semantics due to Theory.join_theory; explicitly check for extend as identity;

clarified -- avoid non-standard extend/merge;

tuned -- avoid non-standard extend;

clarified -- avoid non-standard extend/merge;

proper session imports;

clarified -- avoid non-standard extend;

tuned -- avoid non-standard extend/merge;

prefer conservative extend/merge of theory naming;

support native PID for ML process;

merged

clarified theory data: more robust merge;

proper import sessions;

more thorough extend/merge (for Theory.join_theory);

more thorough extend/merge (for Theory.join_theory);

more thorough extend/merge (for Theory.join_theory);

more thorough extend/merge, notably for master_dir across Theory.join_theory (e.g. for @{file} antiquotation);

more robust: avoid potential problems with encoding of directory name;

tuned grouping

yet another alias

more robust wrt. experimental changes in Poly/ML;

more robust: handle unavailable statistics;

merged

clarified user counters: expose tasks to external monitor;

proper platform path for Windows;

clarified signature;

support for monitoring of external ML process;

clarified signature;

more robust;

support for monitoring of external ML process;

clarified modules: ML_Statistics within bootstrap environment;

misc tuning and modernization;

clarified examples;

concatentation of bit values

prefer canonically oriented lists of bits and more direct characterizations in definitions

more simp rules for concrete numerical values

words added to code generator test

a generic horner sum operation

more thms

clarified message --- as in former ML version (see 940195fbb282);

clarified signature;

clarified messages: avoid duplicate Timing;

clarified messages;

clarified signature;

tuned;

avoid duplicate Timing messages (see also 5c4800f6b25a);

more accurate message;

tuned;

clarified signature;

clarified inlined protocol messages;

removed unused property;

signed_take_bit

more on single-bit operations

proper session Timing for build_history log file (see 5c4800f6b25a);

clarified signature;

more robust, notably for isabelle_cronjob;

more robust build_session protocol: allow prover process to terminate/crash without build_session_finished message;

Update Metis to 2.4

updated to polyml-5.8.1-20200708: recent repository version for testing;

more robust protocol for "Timing ..." messages, notably for pide_session=true;

removed 'freeze_problem_consts' hack in TPTP tools, which wasn't compatible with post-2016 reforms to local theories

separation of traditional bit operations

no pide_session on macos: avoid odd "hang" of remote_build_history;

support generated preferences, i.e. non-strict system options;

factored out auxiliary theory

prefer explicit proof

tuned whitespace;

use less memory on old hardware;

clarified signature;

clarified log message (more uniform);

misc lemma tuning