tuned signature;

provide Isabelle/Electron test;

tuned text;

tuned text;

Tidied up some super-messy proofs

Added a couple of obvious simprules

added lemma

tuned signature: avoid problems with scala3;

proper indentation;

merged

clarified management of interpreter threads: more generic; avoid interp.bind, which is unavailable in scala3;

clarified signature;

clarified signature;

clarified signature, based on hints by IntelliJ IDEA;

tuned signature;

more robust: avoid partiality;

tuned;

clarified signature;

clarified signature;

tuned --- avoid warnings in scala3;

clarified signature;

pass new option only to new version of E

merged

reused slice in Sledgehammer's minimizer

merged

revert 2c861b196d52: still required in HOL/Library/Code_Test.thy;

merged

tuned --- avoid warnings in scala3;

tuned --- avoid redundant patterns;

avoid pattern-match warnings, notably in scala3;

proper type conversion for scala-2.13: problem was unnoticed since ca17e9ebfdf1;

tuned --- accomodate scala3;

proper type conversion for scala-2.13: problem was unnoticed since ca17e9ebfdf1;

back to more ambitious scala-3.1.1 (see 8b7497992301);

tuned --- fewer warnings in scala3;

tuned -- avoid warnings for scala3;

tuned signature -- avoid warnings for scala3;

removed unused flag (see 25c6423ec538);

clarified versions;

documentation on diagnostic devices for code generation

more correct language

enable an E option suggested by Petar Vukmirovic

used HTTPS for SystemOnTPTP

moved from AFP to distribution

avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;

more operations; tuned message: Class.toString already says "class ...";

clarified signature;

tuned: avoid ambiguity in scala3;

clarified signature: avoid ambiguity in scala3;

clarified signature: avoid ambiguity in scala3;

more robust types (for scala3);

tuned for scala3;

proper indentation (relevant for scala3);

adjusted printing of type annotations to accomodate Scala 3

two new examples

pass constructor arity as part of case certficiate

tuned whitespace in generated code

tuned, centralizing case distinction at one place at the cost of modest duplication

clarified formatting, for the sake of scala3;

merged

tuned formatting;

clarified formatting, for the sake of scala3;

tuned

tuned

merge

tuned slices to get the fifth Zipperposition slice in a typical run

merged

tuned sledgehammer documentation

tuned spelling;

merged

updated to scala-parser-combinators 2.1.0, which also fits to scala-3.0.2;

clarified invocation of isabelle.setup.Setup: -classpath allows multiple jars, as required for scala3;

tuned: eliminted do-while for the sake of scala3;

prefer scala 3.0.x, for option "-source 3.0-migration";

tuned: avoid problems with scala3;

tuned: avoid problems with scala3;

provide SCALA_INTERFACES for isabelle_setup;

build Isabelle Scala component from official downloads (for scala-3.1.1);

added documentation

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;

more operations;

tuned signature;

more robust install/uninstall; clarified extension_name (again): --locate-extension wants to see a lowercase name;

more formal extension_manifest, with shasum for sources;

tuned;

tuned signature;

clarified signature;

proper usage;

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

tuned signature;

clarified modules;

tuned signature;

... and removing Primrec from ROOT too

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

merged

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

split veriT reconstruction into Lethe and veriT part

clarified options;

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

clarified options -l vs. -R;

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

proper command-line tool;

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

run Isabelle/VSCode via Scala;

clarified module name;

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

incorporate build_grammar into build_vscode_extension;

removed old generated file;

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;

merged

clarified directory layout and settings: more robust on all platforms;

tuned;

support Electron application framework; clarified vscodium startup;

generated lemma map_ident_strong for BNFs

updated SMT certificates

used more descriptive assert names in SMT-Lib output

clarified and unified executable names;

tuned;

tuned;

merged

suppress OCaml icons: avoid conflict of .ml and .ML, due to case-insensitive file-names in VSCode;

fix handling of lambdas in reconstruction of eq_congruent

more robust: avoid breakdown of Search dialog;

tuned;

always use Isabelle encoding, as in Isabelle/jEdit;

tuned signature;

clarified signature: more uniform ts vs. Scala;

discontinued isabelle_filesystem (superseded by isabelle_encoding), see also da1108a6d249; discontinued special treatment of workspace_dir as session directory;

actually decode/encode symbols;

merged

prefer yarn over npm;

more accurate .hgignore;

clarified startup of "isabelle vscode": vscodium component is required, with patches for Isabelle/VSCode;

tuned messages;

proper init_resources for macos;

clarified names;

clarified modules: vscode vs. extension; clarified signature;

inline Isabelle symbols into source text, so that "isabelle vscode" can start up properly without access to process.env or fs;

more operations;

tuned comments; tuned messages;

patch VSCode source tree to support isabelle_encoding.ts;

more robust, pass "yarn valid-layers-check";

clarified directories;

patch for vscode encoding "UTF-8-Isabelle": clone of "utf8", no symbols yet;

fit into vscode source conventions;

A tiny further cleanup

Tidied some messy proofs

merged

more count_list lemmas

towards UTF-8-Isabelle symbol encoding;

updated to VSCode 1.65.0;

clarified char symbols: cover most European languages;

more elementary Symbol.Matcher without detour via Regex (see also Pure/General/symbol_explode.ML);

tuned comments; tuned imports;

more robust dependencies: avoid implicit update, escpecially of underlying vscode engine;

proper file headers;

added count_list lemmas

tuned message;

more compact result;

prepare patched version more thoroughly, with explicit patches;

tuned signature;

recover platform-specific node binaries from original download, notably for node-pty for Terminal;

tuned message;

tuned;

tuned imports;

misc tuning and clarification;

more executable files; clarified modules;

tuned;

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

split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"

proper name mangling of "undefined" constants in Sledgehammer

earlier availability of lifting

more correct transfer

merged

proper abstraction of function variables when instantiating induction rules in Sledgehammer

added lemma asympD