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

One more instance of Bitbucket in README

remove Bitbucket from website

Update editor instructions for Heptapod + clarifications

Convert maintenance instructions to Heptapod

Update README to Heptapod

Point publish script to heptapod

refactoring

merged

Further Bitbucket -> Heptapod docs update

exclude another session on Mac

Closing branch "devel"

merge

Bitbucket -> Heptapod

Update README for Heptapod

Merge pull request #135 from pclayton/fix-largeword-fromint

Merge pull request #122 from jrtc27/libffi-i386

more CONTRIBUTORS;

Support the "touch" built-in in the interpreter. c.f. ed4fbb81

Remove the PrimIO files from the project. c.f. 16cf8869

merge from afp-2020

point download link to Heptapod

merged

Heptapod acknowledgements

cosmetical change

updated benchmarks

merge from afp-2020

adapted to Isabelle 80d7f004089d