modernized handling of variables

tuned arguments

structurally tuned

tuned names

prefer build combinator

tuned whitespace

tidied up a few proofs

merged

A slightly nicer proof

proper option argument;

tuned signature;

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

tuned signature;

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…

first step in making time slicing more flexible in Sledgehammer: label slices…

updated vscode_extension;

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

merged

tidied and generalised some proofs using small_eqpoll

tidied some proofs

merged

merged

provide pre-built vscodium-1.65.2 for all platforms;

tuned;

clarified options;

provide vscode_extension via component, thus users don't need Node.js…

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

streamlined

extracted selector function, restoring code generation for let expressions

streamlined

disentangled

streamlined

Improved handling splitting theorems in the alphabet command

merged

tuned message;

more operations;

tuned signature;

more robust install/uninstall;

tuned;

more formal extension_manifest, with shasum for sources;

tuned signature;

clarified signature;

tuned -- follow sha1_digest in src/Tools/Setup/src/Build.java;

proper usage;

clarified modules;

tuned signature;

tuned signature;

Removal of the Primrec example in preparation for making it an AFP entry

... and removing Primrec from ROOT too

merged

avoided recomputation in Cooper.djf and ran `isabelle regenerate_cooper`

split veriT reconstruction into Lethe and veriT part

more robust errors -- on foreground process instead of background server;

clarified options;

command-line arguments for "isabelle vscode", similar to "isabelle jedit";

clarified options -l vs. -R;

support console output, e.g. "isabelle vscode -C -- --help";

proper command-line tool;

run Isabelle/VSCode via Scala;

clarified module name;

clean build from explicit MANIFEST: avoid accidental garbage in vsix package;

removed old generated file;

incorporate build_grammar into build_vscode_extension;

hugo site: updated devel info;

hugo site: updated content;

hugo site: restricted generated affiliations;

hugo site: proper ordering;

hugo site: tuned affiliation keys;

hugo site: proper theory view link scrolling;

hugo site: proper topic-only topics page;

Fixed wrong sign handling in fmul-add

hugo site: list sessions separately;

hugo site: tuned;

hugo site: relativize paths;

hugo site: tuned;

hugo site: merge gen and build tool;

hugo site: added doc headers;

Tidied several ugly proofs in some elderly examples

tuned message;

clarified errors;

tuned messages;

support Node.js as well, reusing the engine from Electron/VSCodium;

updated to vscode 1.65.2;

proper result check;