elimination of some needless assumptions

merged

iso lemmas

tuned

tuned

NEWS;

provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored);

adapted to 7b318273a4aa;

cache props;

clarified names; removed remains of old protocol messages;

more thorough protocol_handlers.exit, like file_formats.stop_session;

tuned names;

temporary workaround for 100% CPU usage in OS.Process.sleep;

ML statistics via external process: allows monitoring RTS while ML program sleeps;

clarified catch-all handler --- avoid confusion of Interrupt vs. Exn.Interrupt in varying ML contexts;

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;