2022-03-25 |
blanchet |
cleaned up obsolete E setup and a bit of SPASS
|
file |
diff |
annotate
|
2022-03-25 |
blanchet |
second and last step in making time slicing more flexible in Sledgehammer: try to honor desired slice size
|
file |
diff |
annotate
|
2022-01-31 |
blanchet |
update slice options centrally
|
file |
diff |
annotate
|
2022-01-31 |
blanchet |
further work on new Sledgehammer slicing
|
file |
diff |
annotate
|
2022-01-31 |
blanchet |
tweaked verbose output
|
file |
diff |
annotate
|
2022-01-31 |
blanchet |
tweak padding of prover slice schedule to include all provers
|
file |
diff |
annotate
|
2022-01-31 |
blanchet |
implemented 'max_proofs' mechanism
|
file |
diff |
annotate
|
2022-01-31 |
blanchet |
document new option 'max_proofs'
|
file |
diff |
annotate
|
2022-01-31 |
blanchet |
crude implementation of centralized slicing
|
file |
diff |
annotate
|
2021-05-12 |
wenzelm |
avoid duplicate loading of ML file;
|
file |
diff |
annotate
|
2021-03-12 |
wenzelm |
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
|
file |
diff |
annotate
|
2020-11-12 |
desharna |
Removed development code wrongfully committed
|
file |
diff |
annotate
|
2020-11-05 |
desharna |
Added support for TFX to Sledgehammer
|
file |
diff |
annotate
|
2020-10-08 |
blanchet |
removed support for obsolete prover SNARK and underperforming prover E-Par
|
file |
diff |
annotate
|
2020-10-08 |
desharna |
tune filename
|
file |
diff |
annotate
|
2020-09-08 |
desharna |
[mirabelle] add initial documentation in Sledgehammer's doc
|
file |
diff |
annotate
|
2020-04-23 |
blanchet |
tweaked Vampire's options + tuning
|
file |
diff |
annotate
|
2019-10-25 |
blanchet |
compile
|
file |
diff |
annotate
|
2019-10-25 |
blanchet |
removed E-SInE, a very old system by now (and SInE has been incorporated in many provers in the past decade)
|
file |
diff |
annotate
|
2019-01-06 |
wenzelm |
isabelle update -u path_cartouches;
|
file |
diff |
annotate
|
2016-07-11 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2015-07-18 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
2015-01-29 |
wenzelm |
more explicit indication of Async_Manager_Legacy as Proof General legacy;
|
file |
diff |
annotate
|
2014-11-02 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
2014-09-29 |
blanchet |
made 'moura' tactic more powerful
|
file |
diff |
annotate
|
2014-08-28 |
blanchet |
moved skolem method
|
file |
diff |
annotate
|
2014-08-28 |
blanchet |
added 'skolem' method, esp. for 'obtain's generated from Z3 proofs
|
file |
diff |
annotate
|
2014-08-27 |
blanchet |
renamed new SMT module from 'SMT2' to 'SMT'
|
file |
diff |
annotate
|
2014-06-16 |
blanchet |
fixed parsing of one-argument 'file()' in TSTP files
|
file |
diff |
annotate
|
2014-06-16 |
blanchet |
use right delimiters for Waldmeister proofs
|
file |
diff |
annotate
|
2014-06-16 |
blanchet |
simplified code
|
file |
diff |
annotate
|
2014-06-16 |
blanchet |
moved code around
|
file |
diff |
annotate
|
2014-06-12 |
blanchet |
tuned dependencies
|
file |
diff |
annotate
|
2014-06-11 |
blanchet |
reduces Sledgehammer dependencies
|
file |
diff |
annotate
|
2014-06-11 |
blanchet |
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
|
file |
diff |
annotate
|
2014-06-11 |
blanchet |
removed old SMT module from Sledgehammer
|
file |
diff |
annotate
|
2014-03-14 |
blanchet |
undo rewrite rules (e.g. for 'fun_app') in Isar
|
file |
diff |
annotate
|
2014-03-14 |
blanchet |
more simplification of trivial steps
|
file |
diff |
annotate
|
2014-03-13 |
blanchet |
integrate SMT2 with Sledgehammer
|
file |
diff |
annotate
|
2014-03-13 |
blanchet |
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
|
file |
diff |
annotate
|
2014-02-03 |
blanchet |
renamed ML file
|
file |
diff |
annotate
|
2014-02-03 |
blanchet |
got rid of 'try0' step that is now redundant
|
file |
diff |
annotate
|
2014-01-31 |
blanchet |
moved ML code around
|
file |
diff |
annotate
|
2014-01-31 |
blanchet |
refactor large ML file
|
file |
diff |
annotate
|
2014-01-31 |
blanchet |
renamed many Sledgehammer ML files to clarify structure
|
file |
diff |
annotate
|
2014-01-31 |
blanchet |
renamed ML file
|
file |
diff |
annotate
|
2014-01-31 |
blanchet |
tuned ML file name
|
file |
diff |
annotate
|
2013-12-20 |
blanchet |
reconstruct SPASS-Pirate steps of the form 'x ~= C x' (or more complicated)
|
file |
diff |
annotate
|
2013-07-12 |
wenzelm |
hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
|
file |
diff |
annotate
|
2013-07-12 |
smolkas |
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
|
file |
diff |
annotate
|
2013-07-11 |
smolkas |
optimize isar-proofs by trying different proof methods
|
file |
diff |
annotate
|
2013-07-09 |
smolkas |
moved code -> easier debugging
|
file |
diff |
annotate
|
2013-02-18 |
smolkas |
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
|
file |
diff |
annotate
|
2013-02-18 |
smolkas |
simplified byline, isar_qualifier
|
file |
diff |
annotate
|
2013-02-14 |
smolkas |
renamed sledgehammer_shrink to sledgehammer_compress
|
file |
diff |
annotate
|
2013-01-17 |
smolkas |
move preplaying to own structure
|
file |
diff |
annotate
|
2012-11-28 |
smolkas |
renamed sledgehammer_isar_reconstruct to sledgehammer_proof
|
file |
diff |
annotate
|
2012-11-28 |
smolkas |
put shrink in own structure
|
file |
diff |
annotate
|
2012-11-28 |
smolkas |
put annotate in own structure
|
file |
diff |
annotate
|
2012-10-16 |
blanchet |
added proof minimization code from Steffen Smolka
|
file |
diff |
annotate
|