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

explicit proofs for bit projections

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

a small aggiornamento for Z2

removed superfluous dependency

factored out ancient numeral representation

moved to Word_Lib

more explicit proofs

clarified options --- potentially more robust;

tuned message;