tuned names

prefer build combinator

tuned whitespace

proper option argument;

prefer Isabelle shasum over the old command-line tool with its extra marker character;

tuned signature;

tuned signature; clarified modules;

tuned text, without update of component for now;

omit somewhat pointless integrity check;

tuned;

compile TPTP module

compile mirabelle

further modernized E setup

cleaned up obsolete E setup and a bit of SPASS

second and last step in making time slicing more flexible in Sledgehammer: try to honor desired slice size

first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'

updated vscode_extension;

added parentheses in TPTP output -- seem necessary for some provers

merged

provide pre-built vscodium-1.65.2 for all platforms;

tuned;

provide vscode_extension via component, thus users don't need Node.js development tools; proper default for edit_extension; tuned messages;

clarified options; tuned messages;

Some new library lemmas

merged

really removing Dedekind_real

merged

Moving Dedekind_Real to the AFP

tuned

separated case reduction