#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
185dcd47 |
|
02-Apr-2016 |
wenzelm <none@none> |
prefer infix operations;
|
#
c8a3ab07 |
|
05-Mar-2016 |
wenzelm <none@none> |
tuned signature -- clarified modules; --HG-- rename : src/Pure/Concurrent/time_limit.ML => src/Pure/Concurrent/timeout.ML
|
#
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
|
#
2759308d |
|
25-Sep-2015 |
wenzelm <none@none> |
moved remaining display.ML to more_thm.ML;
|
#
2147d9b6 |
|
22-Jun-2015 |
blanchet <none@none> |
keep 'Pure.all' in goals when preplaying
|
#
13ddea91 |
|
26-Nov-2014 |
wenzelm <none@none> |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
#
6aaa5d2d |
|
24-Sep-2014 |
blanchet <none@none> |
tuning
|
#
86dc3b1a |
|
28-Aug-2014 |
blanchet <none@none> |
made trace more informative when minimization is enabled
|
#
db0c3114 |
|
04-Aug-2014 |
blanchet <none@none> |
slightly earlier exit from preplaying
|
#
d6b75aba |
|
01-Aug-2014 |
blanchet <none@none> |
rationalized preplaying by eliminating (now superfluous) laziness
|
#
0f05e678 |
|
30-Jul-2014 |
blanchet <none@none> |
cascading timeout in parallel evaluation, to rapidly find optimum
|
#
312fdfa6 |
|
21-May-2014 |
blanchet <none@none> |
tuning
|
#
8b8b6855 |
|
13-Mar-2014 |
blanchet <none@none> |
simplified preplaying information
|
#
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
|
#
7f5432b9 |
|
04-Feb-2014 |
blanchet <none@none> |
more generous Isar proof compression -- try to remove failing steps
|
#
484184e5 |
|
04-Feb-2014 |
blanchet <none@none> |
tweaked handling of 'hopeless' methods
|
#
5a7cb477 |
|
03-Feb-2014 |
blanchet <none@none> |
tuning
|
#
71a89b87 |
|
03-Feb-2014 |
blanchet <none@none> |
don't lose additional outcomes
|
#
a2e9e36e |
|
03-Feb-2014 |
blanchet <none@none> |
properly overwrite replay data from one compression iteration to another
|
#
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
|
#
46915898 |
|
03-Feb-2014 |
blanchet <none@none> |
proper fresh name generation
|
#
af459cea |
|
03-Feb-2014 |
blanchet <none@none> |
tuned data structure
|
#
b54f3e71 |
|
03-Feb-2014 |
blanchet <none@none> |
tuned data structure
|
#
a1950e5b |
|
03-Feb-2014 |
blanchet <none@none> |
more flexible compression, choosing whichever proof method works
|
#
88ad28c0 |
|
03-Feb-2014 |
blanchet <none@none> |
less aggressive evaluation
|
#
3da4844f |
|
03-Feb-2014 |
blanchet <none@none> |
tuning
|
#
31457036 |
|
03-Feb-2014 |
blanchet <none@none> |
more thorough, hybrid compression
|
#
0cc92ff3 |
|
03-Feb-2014 |
blanchet <none@none> |
tuning
|
#
c0348805 |
|
03-Feb-2014 |
blanchet <none@none> |
centralize more preplaying
|
#
714b0a4e |
|
03-Feb-2014 |
blanchet <none@none> |
centralize preplaying
|
#
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
|
#
94e4af3c |
|
03-Feb-2014 |
blanchet <none@none> |
merged 'reconstructors' and 'proof methods'
|
#
2bd828a3 |
|
03-Feb-2014 |
blanchet <none@none> |
added 'smt' as a proof method
|
#
58f3d3c0 |
|
02-Feb-2014 |
blanchet <none@none> |
more data structure rationalization
|
#
f7251444 |
|
02-Feb-2014 |
blanchet <none@none> |
more data structure rationalization
|
#
28c29fd3 |
|
02-Feb-2014 |
blanchet <none@none> |
rationalized threading of 'metis' arguments
|
#
ac271564 |
|
02-Feb-2014 |
blanchet <none@none> |
refactored data structure (step 3)
|
#
96efc941 |
|
02-Feb-2014 |
blanchet <none@none> |
refactoring of data structure (step 2)
|
#
a987912b |
|
02-Feb-2014 |
blanchet <none@none> |
unform treatment of preplay_timeout = 0 and > 0
|
#
bcb3a3ff |
|
02-Feb-2014 |
blanchet <none@none> |
refactor data structure (step 1)
|
#
4c95f232 |
|
02-Feb-2014 |
blanchet <none@none> |
tuned code
|
#
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
|
#
5c1d5f08 |
|
31-Jan-2014 |
blanchet <none@none> |
added 'algebra' to the mix
|
#
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
|