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