build Isabelle CSDP component from official downloads;

rebuild component following current "isabelle build_e" and Admin/PLATFORMS;

proper support for Windows/Cygwin;

build Isabelle SPASS component from unofficial download;

tuned;

clarified according to Isabelle_System.download;

misc tuning;

rebuild component following current "isabelle build_e" and Admin/PLATFORMS;

discontinued unused eproof_ram (actually absent in version 2.5);

discontinued obsolete runepar.pl (see 4a3169d8885c);

tuned mirabelle documentation

removed support for obsolete prover SNARK and underperforming prover E-Par

removed spurious documentation item

removed obsolete unmaintained experimental prover Pirate

tune filename

drop obsolete ad hoc support for Satallax isar proof reconstruction

recognize THF proofs properly

typo

LuaLaTeX compatibility improvement

factored out bit comprehension

factored out bit comprehension

Fix formatting of default value in help message of "build_e" component.

LuaLaTeX compatibility improvement

tuned signature;

updated user + host;

updated URL;

clarified multicore options;

discontinued old machines;

updated tests for macOS 10.14 Mojave;

Aded Queues

consolidated for the sake of documentation

a small guide

tuned;

Relational_Disjoint_Set_Forests: minor edits

Relational_Disjoint_Set_Forests: minor additions

Omit the now redundant premise

merged

Simplified some proofs

added lemmas; internalized defn in class

merged

merged

tweaks

merged

still not quite fixed...

A few more reversions

reversion to the explicit existential quantifier

more tidying of messy proofs

clarified signature;

clarified signature;

clarified signature;

clarified signature;

merged

clarified signature;

clarified signature;

LuaLaTeX compatibility improvement

Fix build for module after change to file name for DATE signature.

Change command-line functions to use separate RTS functions rather than a…

Fix interpreted code-generator to handle offsets in addresses as int rather…

Change project file for interpreted version in a similar way to the X86 version.

Change markers for documentation comments.

Add documentation entries to the signatures for PolyDoc. In some cases this…

Add ".sig" as a possible file extension to "use". In PolyML.make try ".sig"…

LuaLaTeX compatibility improvement

merged

merged

de-applying

clarified arm64-linux base line: prefer Pi OS, which is based on slightly older…

detect/guess arm32 platform (unsupported);

build component according to "isabelle build_e -V 2.5" (inactive);

updated component according to "isabelle build_e -V 2.0";

proper usage;

clarified;

merged

clarified installed files;

build Isabelle E prover component from official downloads;

clarified signature;

updated for coming release;

updated to current cygwin-20201002, after 3.1.7-1 from 24-Aug-2020;

clarified platforms;

updated to opam-2.0.7;

merged

fixed a bunch of ugly proofs

Add more tacing to sledgehammer_isar_trace

support arm64-linux Poly/ML (slow bytecode interpreter only);

purge arm64-linux --- no build_release support yet;

more systematic platform support, including arm64-linux;

tuned according to hints by IntelliJ IDEA;

updated certificates to make it work again after recent changes to smt/z3 setup;

merged

clarified signature;

updated to sqlite-jdbc-3.32.3.2;

build Isabelle sqlite-jdbc component from official download;

support arm64-linux;

detect arm64-linux platform;

Effectively disable timeout for smt method/tactic

[mirabelle] add initial documentation in Sledgehammer's doc

clarified signature;

clarified names;

tuned signature;

formal platform information, notably for ssh;