merged

tuned sledehammer to return best succeeding preplay method

expanded sledgehammer's expect option with some_preplayed

added preplay results to sledgehammer_output

tuned sledgehammer to suggest (smt (verit)) on failing smt preplay for all but Z3

further tweaked E's setup

tweaked E setup

merged

post-merged into new Lethe code

merged

fixed generation of Isar proofs e89709b80b6e

NEWS and CONTRIBUTORS

nicer TPTP output

regenerated

tighter check to ensure that patterns remain left-linear, previous implementation was overcautious

tuned

tuned

separated treatment of undefined bodys

tuned arguments

modernized handling of variables

structurally tuned

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

separated selector function entirely

self-contained extraction auf clauses

extracted selector function, restoring code generation for let expressions

streamlined

streamlined

streamlined

disentangled

merged

tuned message;