| #
daac7840 |
|
07-Aug-2017 |
blanchet <none@none> |
tuning imports
|
| #
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
9dce0aeb |
|
20-Sep-2014 |
steckerm <none@none> |
Changed proof method to auto for custom Waldmeister lemma
|
| #
058efb97 |
|
20-Sep-2014 |
steckerm <none@none> |
Minor fixes in ATP_Waldmeister
|
| #
8666297f |
|
02-Sep-2014 |
steckerm <none@none> |
Some work on the new waldmeister integration
|
| #
fa2cfdb9 |
|
30-Jul-2014 |
fleury <none@none> |
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
|
| #
688959b7 |
|
30-Jul-2014 |
fleury <none@none> |
imported patch hilbert_choice_support
|
| #
50e7dab8 |
|
30-Jul-2014 |
fleury <none@none> |
imported patch satallax_proof_support_Sledgehammer
|
| #
dd2a0d80 |
|
16-Jun-2014 |
blanchet <none@none> |
simplified code
|
| #
07041a99 |
|
16-Jun-2014 |
blanchet <none@none> |
moved code around
--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_prover_waldmeister.ML => src/HOL/Tools/ATP/atp_waldmeister.ML
|
| #
c42c063d |
|
16-Jun-2014 |
fleury <none@none> |
add support for Isar reconstruction for thf1 ATP provers like Leo-II.
|
| #
67048627 |
|
13-May-2014 |
blanchet <none@none> |
hide more internal names
|
| #
6d11884a |
|
18-Oct-2013 |
blanchet <none@none> |
killed more "no_atp"s
|
| #
d85019cb |
|
09-Sep-2013 |
blanchet <none@none> |
move metis to new monomorphizer
|
| #
e26a601f |
|
28-Mar-2013 |
boehmes <none@none> |
new, simpler implementation of monomorphization;
old monomorphization code is still available as Legacy_Monomorphization;
modified SMT integration to use the new monomorphization code
|
| #
e3227796 |
|
22-Aug-2012 |
wenzelm <none@none> |
prefer ML_file over old uses;
|
| #
0c3297b3 |
|
21-May-2012 |
blanchet <none@none> |
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
|
| #
678bfbab |
|
23-Jan-2012 |
blanchet <none@none> |
renamed two files to make room for a new file
--HG--
rename : src/HOL/Tools/ATP/atp_translate.ML => src/HOL/Tools/ATP/atp_problem_generate.ML
rename : src/HOL/Tools/ATP/atp_reconstruct.ML => src/HOL/Tools/ATP/atp_proof_reconstruct.ML
rename : src/HOL/Tools/ATP/atp_redirect.ML => src/HOL/Tools/ATP/atp_proof_redirect.ML
rename : src/HOL/Tools/Metis/metis_translate.ML => src/HOL/Tools/Metis/metis_generate.ML
|
| #
d9151191 |
|
14-Dec-2011 |
blanchet <none@none> |
added new proof redirection code
|
| #
f7a23077 |
|
16-Nov-2011 |
blanchet <none@none> |
compile
|
| #
70c7dd0c |
|
09-Aug-2011 |
blanchet <none@none> |
load lambda-lifting structure earlier, so it can be used in Metis
|
| #
2d869fab |
|
05-Jul-2011 |
nik <none@none> |
improved translation of lambdas in THF
|
| #
41a0ce3b |
|
31-May-2011 |
blanchet <none@none> |
use "monomorph.ML" in "ATP" theory (so the new Metis can use it)
|
| #
47a925bb |
|
31-May-2011 |
blanchet <none@none> |
first step in sharing more code between ATP and Metis translation
--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML => src/HOL/Tools/ATP/atp_reconstruct.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML => src/HOL/Tools/ATP/atp_translate.ML
|
| #
0891da48 |
|
25-Oct-2010 |
blanchet <none@none> |
reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
|
| #
a9beedd9 |
|
25-Oct-2010 |
haftmann <none@none> |
moved sledgehammer to Plain; tuned dependencies
|
| #
08256a7d |
|
04-Oct-2010 |
blanchet <none@none> |
tuned comments
|
| #
79078c7d |
|
05-Oct-2010 |
blanchet <none@none> |
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
|