isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

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

support for PDF.js: platform-independent PDF viewer;
5 months ago, by wenzelm
more robust mime_type;
5 months ago, by wenzelm
merged
5 months ago, 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;
5 months ago, by wenzelm
one new lemma
5 months ago, by paulson
clarified options;
5 months ago, by wenzelm
clarified options;
5 months ago, by wenzelm
clarified directory;
5 months ago, by wenzelm
tuned whitespace;
5 months ago, by wenzelm
prefer strict equality, without implicit type conversion;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
auto-update by VSCode;
5 months ago, by wenzelm
more activationEvents, as proposed by Denis Paluca;
5 months ago, by wenzelm
tuned message;
5 months ago, by wenzelm
NEWS;
5 months ago, by wenzelm
run Isabelle/VSCode using local VSCodium installation;
5 months ago, by wenzelm
provide macos_exe, based on bin/codium from linux;
5 months ago, by wenzelm
clarified options;
5 months ago, by wenzelm
Avoid overaggresive splitting.
5 months ago, by haftmann
more lemmas for distribution
5 months ago, by haftmann
Avoid overaggresive simplification.
5 months ago, by haftmann
merged
5 months ago, by wenzelm
setup VSCode from VSCodium distribution;
5 months ago, by wenzelm
more robust package_dir, to increase chances that it works with IntelliJ IDEA;
5 months ago, by wenzelm
NEWS
5 months ago, by desharna
Mirabelle now considers goals preceding "unfolding" and "using" commands
5 months ago, by desharna
merged
5 months ago, by paulson
an assortment of new or stronger lemmas
5 months ago, by paulson
obsolete (reverting b3d6bb2ebf77): Isabelle/Naproche cache is now value-oriented;
5 months ago, by wenzelm
print outcome of Sledgehammer search in panel
5 months ago, by blanchet
print Sledgehammer error message
5 months ago, by blanchet
updated documentation to current matter of affairs
6 months ago, by haftmann
unused;
6 months ago, by wenzelm
clarified signature;
6 months ago, by wenzelm
merged
6 months ago, by desharna
added Isabelle identification to Mirabelle output
6 months ago, by desharna
uniformized fact selection for ATP and SMT in Sledgehammer
6 months ago, by desharna
provide cache for slow computations;
6 months ago, by wenzelm
used max_facts and fact_filter from slice for both ATP and SMT in sledgehammer
6 months ago, by desharna
more operations;
6 months ago, by wenzelm
more liberal parsing of Sledgehammer options to allow empty lists (as suggested by Larry Paulson)
6 months ago, by blanchet
more robust TSTP proof parsing
6 months ago, by blanchet
added possibility of extra options to SMT slices
6 months ago, by blanchet
tuned output syntax: Hoare triples are now blocks
6 months ago, by nipkow
tuned output syntax: INV and VAR are now blocks
6 months ago, by nipkow
more precise slicing computation and output when not enough lemmas are available (e.g. with the 'only' syntax 'sledgehammer (lem1 lem2 lem3)')
6 months ago, by blanchet
enable induction in one of Zipperposition's slices
6 months ago, by blanchet
made sorting of Vampire facts more robust in the face of names that deviate from the standard scheme
6 months ago, by blanchet
robustly handle empty proof blocks in Isar proof output
6 months ago, by blanchet
propagate right result when enough proofs have been found
6 months ago, by blanchet
correctly parse E proofs that assume '=' and '!=' bind more tightly than connectives
6 months ago, by blanchet
don't lose error messages
6 months ago, by blanchet
don't pass --auto-schedule to E indiscriminately -- use it instead of 'auto' in one slice
6 months ago, by blanchet
careful with partial applications
6 months ago, by blanchet
don't perform preplaying steps if preplaying is disabled
6 months ago, by blanchet
adjust TPTP THF parser to give priority to @ over other operators, to parse Ehoh proofs
6 months ago, by blanchet
tuned punctuation
6 months ago, by blanchet
handle TPTP '!=' more gracefully in Isar proof reconstruction
6 months ago, by blanchet
guard against duplicate lines in Zipperposition proofs
6 months ago, by blanchet
tuning
6 months ago, by blanchet

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 tip

isabelle