isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -120 +120 +1000 +3000 tip

tuned;
2022-02-28, by wenzelm
tuned;
2022-02-28, by wenzelm
tuned message;
2022-02-28, by wenzelm
disable extension updates;
2022-02-28, by wenzelm
tuned message;
2022-02-28, by wenzelm
disable check for updates: support just one static version;
2022-02-28, by wenzelm
misc tuning based on comments by Heiko Eißfeldt;
2022-02-27, by wenzelm
misc tuning based on comments by Heiko Eißfeldt;
2022-02-27, by wenzelm
removed junk;
2022-02-26, by wenzelm
some updates to README.md;
2022-02-26, by wenzelm
clarified default settings;
2022-02-26, by wenzelm
tuned whitespace;
2022-02-26, by wenzelm
support Isabelle fonts via patch of vscode resources;
2022-02-26, by wenzelm
proper Presentation.Entity_Context for hyperlinks (amending da1108a6d249);
2022-02-25, by wenzelm
clarified symbolic path;
2022-02-25, by wenzelm
clarified extension name (again);
2022-02-25, by wenzelm
removed obsolete material;
2022-02-25, by wenzelm
update scripts, based on recent "yo code" template;
2022-02-25, by wenzelm
clarified extension name (again), corresponding to qualified resources within VSCode (settings, commands, etc.);
2022-02-25, by wenzelm
clarified signature;
2022-02-25, by wenzelm
clarified extension name;
2022-02-25, by wenzelm
clarified signature;
2022-02-25, by wenzelm
clarified signature;
2022-02-25, by wenzelm
clarified options;
2022-02-25, by wenzelm
support local .vsix installation;
2022-02-25, by wenzelm
formal record of generated package-lock.json;
2022-02-25, by wenzelm
pro-forma update of version, for ongoing development;
2022-02-25, by wenzelm
updated notes on Isabelle/VSCode development;
2022-02-25, by wenzelm
proper engines.vscode (amending c04ccea8bdd2): required for "vsce package", e.g. via "isabelle build_vscode;
2022-02-25, by wenzelm
simp rules for negative numerals
2022-02-24, by haftmann
updated vscode extension: proper recoding;
2022-02-23, by Fabian Huch
tuned vscode extension;
2022-02-23, by Fabian Huch
tuned vscode extension: split isabelle fsp into workspace and mapping;
2022-02-23, by Fabian Huch
update VSCode plugin dependencies;
2022-02-23, by Fabian Huch
added Isabelle output panel to VSCode extension;
2022-02-23, by Fabian Huch
Simplified a couple of extremely long and ugly apply-proofs
2022-02-23, by paulson
merged
2022-02-22, by wenzelm
some updates to README.md;
2022-02-22, by wenzelm
refer to Isabelle settings via environment, which is provided via "isabelle vscode";
2022-02-22, by wenzelm
more operations;
2022-02-22, by wenzelm
more robust startup wrt. VSCode workspace (by Fabian Huch);
2022-02-22, by wenzelm
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
2022-02-22, by wenzelm
have Sledgehammer honor 'smt_nat_as_int' option
2022-02-22, by blanchet
more handling of Zipperposition definitions in Isar proof construction
2022-02-22, by blanchet
handle Zipperposition definitions in Isar proof construction
2022-02-22, by blanchet
parse Zipperposition definitions
2022-02-22, by blanchet
clarified URL;
2022-02-21, by wenzelm
clarified pdf path;
2022-02-21, by wenzelm
HTTP view of Isabelle PDF documentation;
2022-02-21, by wenzelm
clarified signature;
2022-02-21, by wenzelm
more robust;
2022-02-21, by wenzelm
tuned message;
2022-02-21, by wenzelm
clarified signature: more explicit section structure;
2022-02-21, by wenzelm
clarified signature;
2022-02-21, by wenzelm
clarified signature;
2022-02-21, by wenzelm
tuned signature;
2022-02-21, by wenzelm
tuned;
2022-02-21, by wenzelm
clarified URL (again);
2022-02-21, by wenzelm
more robust toplevel url: allow extra "/";
2022-02-21, by wenzelm
clarified signature;
2022-02-21, by wenzelm
clarified signature;
2022-02-20, by wenzelm
clarified signature;
2022-02-20, by wenzelm
support for PDF.js: platform-independent PDF viewer;
2022-02-20, by wenzelm
more robust mime_type;
2022-02-20, by wenzelm
merged
2022-02-18, by wenzelm
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;
2022-02-18, by wenzelm
one new lemma
2022-02-18, by paulson
clarified options;
2022-02-18, by wenzelm
clarified options;
2022-02-18, by wenzelm
clarified directory;
2022-02-18, by wenzelm
tuned whitespace;
2022-02-18, by wenzelm
prefer strict equality, without implicit type conversion;
2022-02-18, by wenzelm
tuned;
2022-02-18, by wenzelm
auto-update by VSCode;
2022-02-18, by wenzelm
more activationEvents, as proposed by Denis Paluca;
2022-02-18, by wenzelm
tuned message;
2022-02-18, by wenzelm
NEWS;
2022-02-18, by wenzelm
run Isabelle/VSCode using local VSCodium installation;
2022-02-18, by wenzelm
provide macos_exe, based on bin/codium from linux;
2022-02-18, by wenzelm
clarified options;
2022-02-18, by wenzelm
Avoid overaggresive splitting.
2022-02-17, by haftmann
more lemmas for distribution
2022-02-17, by haftmann
Avoid overaggresive simplification.
2022-02-17, by haftmann
merged
2022-02-17, by wenzelm
setup VSCode from VSCodium distribution;
2022-02-17, by wenzelm
more robust package_dir, to increase chances that it works with IntelliJ IDEA;
2022-02-17, by wenzelm
NEWS
2022-02-16, by desharna
Mirabelle now considers goals preceding "unfolding" and "using" commands
2022-02-16, by desharna
merged
2022-02-15, by paulson
an assortment of new or stronger lemmas
2022-02-15, by paulson
obsolete (reverting b3d6bb2ebf77): Isabelle/Naproche cache is now value-oriented;
2022-02-15, by wenzelm
print outcome of Sledgehammer search in panel
2022-02-14, by blanchet
print Sledgehammer error message
2022-02-14, by blanchet
updated documentation to current matter of affairs
2022-02-12, by haftmann
unused;
2022-02-10, by wenzelm
clarified signature;
2022-02-10, by wenzelm
merged
2022-02-10, by desharna
added Isabelle identification to Mirabelle output
2022-02-09, by desharna
uniformized fact selection for ATP and SMT in Sledgehammer
2022-02-09, by desharna
provide cache for slow computations;
2022-02-09, by wenzelm
used max_facts and fact_filter from slice for both ATP and SMT in sledgehammer
2022-02-09, by desharna
more operations;
2022-02-09, by wenzelm
more liberal parsing of Sledgehammer options to allow empty lists (as suggested by Larry Paulson)
2022-02-09, by blanchet
more robust TSTP proof parsing
2022-02-07, by blanchet
added possibility of extra options to SMT slices
2022-02-07, by blanchet
tuned output syntax: Hoare triples are now blocks
2022-02-04, by nipkow
tuned output syntax: INV and VAR are now blocks
2022-02-03, by nipkow
more precise slicing computation and output when not enough lemmas are available (e.g. with the 'only' syntax 'sledgehammer (lem1 lem2 lem3)')
2022-02-02, by blanchet
enable induction in one of Zipperposition's slices
2022-02-02, by blanchet
made sorting of Vampire facts more robust in the face of names that deviate from the standard scheme
2022-02-01, by blanchet
robustly handle empty proof blocks in Isar proof output
2022-02-01, by blanchet
propagate right result when enough proofs have been found
2022-02-01, by blanchet
correctly parse E proofs that assume '=' and '!=' bind more tightly than connectives
2022-02-01, by blanchet
don't lose error messages
2022-02-01, by blanchet
don't pass --auto-schedule to E indiscriminately -- use it instead of 'auto' in one slice
2022-02-01, by blanchet
careful with partial applications
2022-02-01, by blanchet
don't perform preplaying steps if preplaying is disabled
2022-02-01, by blanchet
adjust TPTP THF parser to give priority to @ over other operators, to parse Ehoh proofs
2022-02-01, by blanchet
tuned punctuation
2022-02-01, by blanchet
handle TPTP '!=' more gracefully in Isar proof reconstruction
2022-02-01, by blanchet