more thorough extend/merge, notably for master_dir across Theory.join_theory (e.

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

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

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

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;

Add a related check for offsets that could exceed a signed 32-bit value.

Short constant index values can be put into the offset but leave larger and…

Modify test so that it works if int is IntInf.int.

merge from afp-2020

update maintenance docs

concatentation of bit values

concatentation of bit values

saturation framework: renamings

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

more simp rules for concrete numerical values

words added to code generator test

prefer canonically oriented lists of bits in definitions

a generic horner sum operation

more thms

more realistic timeout: 20min CPU time;

tuned whitespace;

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

clarified signature;

clarified messages: avoid duplicate Timing;

clarified messages;

tuned;

clarified signature;

more accurate message;

avoid duplicate Timing messages (see also 5c4800f6b25a);

tuned;

clarified signature;

clarified inlined protocol messages;

removed unused property;

more on single-bit operations

signed_take_bit

signed_take_bit

Add new material, mostly centered around cartesian categories. Sync with my…

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…

Fix failing proofs after update to Metis 2.4

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…

Convert single bindings from mutual recursion into simple bindings.

The "setter" for a container refers to the container itself so any bindings…

Fix function name: they're mutual bindings not mutable.

When analysing the usage pattern of a recursive function we need to consider…

Fix use of "print" rather than "stream" for debugging.

separation of traditional bit operations

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

factored out auxiliary theory

more operations for maps

tuned whitespace;

clarified signature;

use less memory on old hardware;

clarified log message (more uniform);

misc lemma tuning

explicit proofs for bit projections

misc lemma tuning

activated simproc defined_all

extraction of equations x = t from premises beneath meta-all

updated documentation

obsolete duplicates

removed superfluous dependency

a small aggiornamento for Z2

factored out ancient numeral representation

moved to Word_Lib

tuned whitespace

factored out ancient numeral representation

moved to Word_Lib

more explicit proofs

clarified options --- potentially more robust;

tuned message;

clarified signature;

merge from afp-2020

Update history commit links to Heptapod

Error message update

merge from afp-2020