| #
9d709195 |
|
17-May-2016 |
blanchet <none@none> |
proper consideration of chained facts in 'try0' minimization
|
| #
185dcd47 |
|
02-Apr-2016 |
wenzelm <none@none> |
prefer infix operations;
|
| #
456ff485 |
|
01-Feb-2016 |
blanchet <none@none> |
preplaying of 'smt' and 'metis' more in sync with actual method
|
| #
5cbf1a62 |
|
01-Feb-2016 |
blanchet <none@none> |
preplaying of 'smt' and 'metis' more in sync with actual method
|
| #
0ef6756d |
|
02-Oct-2015 |
blanchet <none@none> |
further reduced dependency on legacy async thread manager
|
| #
71c619a0 |
|
28-May-2015 |
blanchet <none@none> |
took out Sledgehammer minimizer optimization that breaks things
|
| #
5b07dac6 |
|
28-Aug-2014 |
blanchet <none@none> |
removed show stuttering
|
| #
86dc3b1a |
|
28-Aug-2014 |
blanchet <none@none> |
made trace more informative when minimization is enabled
|
| #
32b98073 |
|
28-Aug-2014 |
blanchet <none@none> |
tuned tracing output (indirectly)
|
| #
2e7a0295 |
|
04-Aug-2014 |
blanchet <none@none> |
sort facts in minimizer as well
|
| #
be9737d8 |
|
24-Jul-2014 |
blanchet <none@none> |
faster minimization by not adding facts that are already in the simpset
|
| #
4a5e0afe |
|
01-Aug-2014 |
blanchet <none@none> |
tuning
|
| #
2d933a72 |
|
01-Aug-2014 |
blanchet <none@none> |
simplified minimization logic
|
| #
cbb0de62 |
|
01-Aug-2014 |
blanchet <none@none> |
tuning
|
| #
61286368 |
|
30-Jul-2014 |
blanchet <none@none> |
tuned ML function name
|
| #
312fdfa6 |
|
21-May-2014 |
blanchet <none@none> |
tuning
|
| #
cf3941c9 |
|
13-Feb-2014 |
blanchet <none@none> |
avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures
|
| #
7c9121a5 |
|
04-Feb-2014 |
blanchet <none@none> |
tuned slack
|
| #
5a7cb477 |
|
03-Feb-2014 |
blanchet <none@none> |
tuning
|
| #
fb11429b |
|
03-Feb-2014 |
blanchet <none@none> |
generate comments in Isar proofs
|
| #
597d2bf4 |
|
03-Feb-2014 |
blanchet <none@none> |
keep all proof methods in data structure until the end, to enhance debugging output
|
| #
af459cea |
|
03-Feb-2014 |
blanchet <none@none> |
tuned data structure
|
| #
a1950e5b |
|
03-Feb-2014 |
blanchet <none@none> |
more flexible compression, choosing whichever proof method works
|
| #
0cc92ff3 |
|
03-Feb-2014 |
blanchet <none@none> |
tuning
|
| #
c0348805 |
|
03-Feb-2014 |
blanchet <none@none> |
centralize more preplaying
|
| #
b8ffece8 |
|
03-Feb-2014 |
blanchet <none@none> |
tuning
|
| #
714b0a4e |
|
03-Feb-2014 |
blanchet <none@none> |
centralize preplaying
|
| #
fcc30082 |
|
03-Feb-2014 |
blanchet <none@none> |
tuned
|
| #
700f2e9d |
|
03-Feb-2014 |
blanchet <none@none> |
renamed ML file
--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML => src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
|
| #
58f3d3c0 |
|
02-Feb-2014 |
blanchet <none@none> |
more data structure rationalization
|
| #
49e83bed |
|
02-Feb-2014 |
blanchet <none@none> |
tuning
|
| #
f7251444 |
|
02-Feb-2014 |
blanchet <none@none> |
more data structure rationalization
|
| #
96efc941 |
|
02-Feb-2014 |
blanchet <none@none> |
refactoring of data structure (step 2)
|
| #
bcb3a3ff |
|
02-Feb-2014 |
blanchet <none@none> |
refactor data structure (step 1)
|
| #
47bd3a59 |
|
02-Feb-2014 |
blanchet <none@none> |
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
|
| #
91ba1387 |
|
02-Feb-2014 |
blanchet <none@none> |
reset timing information after changes
|
| #
348374bc |
|
31-Jan-2014 |
blanchet <none@none> |
generalized preplaying infrastructure to store various results for various methods
|
| #
33d1a2d4 |
|
31-Jan-2014 |
blanchet <none@none> |
tuning
|
| #
70b7915d |
|
31-Jan-2014 |
blanchet <none@none> |
tuned ML function names
|
| #
fed5d9bd |
|
31-Jan-2014 |
blanchet <none@none> |
tuning
|
| #
eb52da60 |
|
31-Jan-2014 |
blanchet <none@none> |
renamed many Sledgehammer ML files to clarify structure
--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_run.ML => src/HOL/Tools/Sledgehammer/sledgehammer.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_print.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_print.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML => src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
|