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
+1000
+3000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
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
guard against duplicate lines in Zipperposition proofs
2022-02-01, by blanchet
tuning
2022-02-01, by blanchet
tuned NEWS
2022-02-01, by blanchet
compile HOL-TPTP
2022-01-31, by blanchet
compile Metis_Examples
2022-01-31, by blanchet
more NEWS
2022-01-31, by blanchet
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
tip