direct exit to theory when ending nested target on theory target

tuned

consolidated terminology

avoid baroque export

clarified message;

tuned signature;

clarified options;

clarified signature: allow complex bash script;

more explicit MinGW context;

more standard path output (despite platform_path from d55eb82ae77b);

clarified signature;

clarified errors;

tuned signature;

more explicit MinGW context;

more libs for build_csdp;

support for MSYS2/MinGW64 on Windows;

tuned --- according to instructions on Website;

updated to csdp-6.1.1, with support for arm64-linux;

proper support for x86_64-windows via msys/mingw64;

more standard build from sources;

tuned message;

component csdp-6.2.0 for testing: example #2 in theory HOL-ex.SOS fails with…

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;