tuned output;

clarified signature;

tuned, based on suggestions by IntelliJ IDEA;

tuned;

clarified command-line options;

update official Isabelle release, notably for "Admin/init -R";

more robust;

build component for VSCodium (cross-compiled from sources for all platforms);

tuned signature: more robust operation;

clarified order;

proper antiquotations (amending ff784d5a5bfb);

clarified signature: file operations take standard_path as in Isabelle/ML/Scala;

provide symbols statically via ISABELLE_VSCODE_WORKSPACE, instead of LSP/PIDE protocol;

proper init of non-existing file;

proper function call;

clarified signature;

tuned;

tuned, based on suggestions by IntelliJ IDEA;

tuned;

clarified signature;

clarified modules: more uniform .scala vs. ts (amending 4519eeefe3b5);

misc tuning, based on suggestions by IntelliJ IDEA;

clarified signature;

tuned signature;

clarified signature; clarified data structures;

tuned imports;

clarified signature;

clarified signature;

tuned signature;

misc tuning, based on suggestions by IntelliJ IDEA;

clarified modules;

support for file-system operations;

tuned signature;

follow standard Isabelle license --- no longer published on market place;

tuned README;

disregard public marketplace;

tuned imports;

more robust;

merged

tuned message;

clarified module;

tuned comments;

added documentation for new VSCode modules;

proper monospace font for terminal;

merged

tuned;

support system path representations (as in Isabelle/Java/Scala);

auto-update;

more robust;

clarified modules;

clarified rendering;

prefer hardwired locale;

more aggressive activation;

Added some theorems (from Wetzel)

tuned;

tuned;

tuned message;

disable extension updates;

tuned message;

disable check for updates: support just one static version;

misc tuning based on comments by Heiko Eißfeldt;

misc tuning based on comments by Heiko Eißfeldt;

removed junk;

some updates to README.md;

clarified default settings;

tuned whitespace;

support Isabelle fonts via patch of vscode resources;

proper Presentation.Entity_Context for hyperlinks (amending da1108a6d249);

clarified symbolic path;

clarified extension name (again);

removed obsolete material;

update scripts, based on recent "yo code" template;

clarified extension name (again), corresponding to qualified resources within VSCode (settings, commands, etc.);

clarified signature;

clarified extension name;

clarified signature;

clarified signature;

clarified options;

support local .vsix installation; discontinued publishing to VSCode Marketplace, which will become obsolete eventually;

formal record of generated package-lock.json;

pro-forma update of version, for ongoing development;

updated notes on Isabelle/VSCode development;

proper engines.vscode (amending c04ccea8bdd2): required for "vsce package", e.g. via "isabelle build_vscode;

simp rules for negative numerals

updated vscode extension: proper recoding;

tuned vscode extension;

tuned vscode extension: split isabelle fsp into workspace and mapping;

update VSCode plugin dependencies;

added Isabelle output panel to VSCode extension;

Simplified a couple of extremely long and ugly apply-proofs

merged

some updates to README.md;

refer to Isabelle settings via environment, which is provided via "isabelle vscode"; clarified error handling;

more operations;

more robust startup wrt. VSCode workspace (by Fabian Huch);

various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);

have Sledgehammer honor 'smt_nat_as_int' option

more handling of Zipperposition definitions in Isar proof construction

handle Zipperposition definitions in Isar proof construction

parse Zipperposition definitions

clarified URL;

clarified pdf path;

HTTP view of Isabelle PDF documentation;

clarified signature;

more robust;

tuned message;

clarified signature: more explicit section structure;

clarified signature;

clarified signature;

tuned signature;

tuned;

clarified URL (again);

more robust toplevel url: allow extra "/";

clarified signature;

clarified signature; clarified URLs;

clarified signature;

support for PDF.js: platform-independent PDF viewer;

more robust mime_type;

merged

improved support for Java Chromium Embedded Framework (JCEF): works on x86_64-linux and x86_64-windows with jdk-15 (not jdk-17), does not work on arm64 and darwin;

one new lemma

clarified options;

clarified options;

clarified directory;

tuned whitespace;

prefer strict equality, without implicit type conversion;

tuned;

auto-update by VSCode;

more activationEvents, as proposed by Denis Paluca;

tuned message;

NEWS;

run Isabelle/VSCode using local VSCodium installation;

provide macos_exe, based on bin/codium from linux;

clarified options;

Avoid overaggresive splitting.

more lemmas for distribution

Avoid overaggresive simplification.

merged

setup VSCode from VSCodium distribution;

more robust package_dir, to increase chances that it works with IntelliJ IDEA;

NEWS

Mirabelle now considers goals preceding "unfolding" and "using" commands

merged

an assortment of new or stronger lemmas

obsolete (reverting b3d6bb2ebf77): Isabelle/Naproche cache is now value-oriented;

print outcome of Sledgehammer search in panel

print Sledgehammer error message

updated documentation to current matter of affairs

unused;

clarified signature;

merged

added Isabelle identification to Mirabelle output

uniformized fact selection for ATP and SMT in Sledgehammer

provide cache for slow computations;

used max_facts and fact_filter from slice for both ATP and SMT in sledgehammer

more operations;

more liberal parsing of Sledgehammer options to allow empty lists (as suggested by Larry Paulson)

more robust TSTP proof parsing

added possibility of extra options to SMT slices

tuned output syntax: Hoare triples are now blocks

tuned output syntax: INV and VAR are now blocks

more precise slicing computation and output when not enough lemmas are available (e.g. with the 'only' syntax 'sledgehammer (lem1 lem2 lem3)')

enable induction in one of Zipperposition's slices

made sorting of Vampire facts more robust in the face of names that deviate from the standard scheme

robustly handle empty proof blocks in Isar proof output

propagate right result when enough proofs have been found

correctly parse E proofs that assume '=' and '!=' bind more tightly than connectives

don't lose error messages

don't pass --auto-schedule to E indiscriminately -- use it instead of 'auto' in one slice

careful with partial applications

don't perform preplaying steps if preplaying is disabled

adjust TPTP THF parser to give priority to @ over other operators, to parse Ehoh proofs

tuned punctuation

handle TPTP '!=' more gracefully in Isar proof reconstruction

guard against duplicate lines in Zipperposition proofs

tuning

tuned NEWS

compile HOL-TPTP

compile Metis_Examples

more NEWS

compile mirabelle

tweaked Auto Sledgehammer's behavior and output

updated NEWS

removed experimental prover z3_tptp

print more verbose information

run all installed provers by default

update slice options centrally

further work on new Sledgehammer slicing

tweaked verbose output

tweak padding of prover slice schedule to include all provers

implemented 'max_proofs' mechanism

document new option 'max_proofs'

crude implementation of centralized slicing

removed obscure E option

take 'induction_rules' into consideration, as well as 'max_facts' even when 'only' is set

rationalize slicing format

thread slices through

simplified 'best_slice' data structure and made minor changes to slices

changed logic of 'slice' option to 'slices'

updated documentation of 'slice' (now 'slices') option

revised Sledgehammer documentation

rationalized output for forthcoming slicing model

use same default for FO and HO provers w.r.t. induction principles, based on evaluation -- this also simplifies the code

disable slicing within ATP module (in preparation for refactoring)

disable slicing within SMT (in preparation for factoring it out)

generalized the 'slice' option towards more flexible slicing

tuned -- fewer warnings;

Added a tiny proof

Deletion of a duplicate proof

useful lemma integral_less

merged

removed unused parameter following f9908452b282

treat 'using X by meson' as 'by (meson X)' to avoid loss of polymorphism (cf. metis)

fixed dodgy intro! attributes

merged

optimized facts traversal in TPTP translation

optimized app_op_level selection in TPTP generation

tuned trivial check in mirabelle_sledgehammer

renamed run_action to run in Mirabelle.action record

added spying of fact filtering timing

tuned mirabelle_sledgehammer output

added spying to Sledgehammer

proper fact filter for dummy ATPs

added syping of fact filtering time to sledgehammer

removed unsynchronized references in mirabelle_sledgehammer

tuned mirabelle_sledgehammer to have a single call to Synchronized.change per run

updated to polyml-test-15c840d48c9a;

some updates and clarification on Assumption.export_term;

new theorem has_integral_UN

updated to jdk-17.0.2+8;

used elapsed time instead of cpu time in Mirabelle because the latter contain cpu time of all threads

NEWS

added Mirabelle option "-y" for dry run

tuned garbage optimization

added cpu time (in ms) to Mirabelle run_action output

added Mirabelle option -r to randomize the goals before selection

A new lemma about inverse image

proper treatment of $let variables in symbol table in Sledgehammer

removed unconditional TPTP symbol declaration for undefined_bool in sledgehammer

merged