#
e60cf64d |
|
06-Jan-2019 |
wenzelm <none@none> |
isabelle update -u path_cartouches;
|
#
c5b12b18 |
|
25-Mar-2016 |
wenzelm <none@none> |
avoid hardwired values;
|
#
cf373f71 |
|
18-Mar-2016 |
wenzelm <none@none> |
clarified print depth;
|
#
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
d432bf2b |
|
29-Oct-2014 |
wenzelm <none@none> |
modernized setup;
|
#
67048627 |
|
13-May-2014 |
blanchet <none@none> |
hide more internal names
|
#
2a0d4ed7 |
|
25-Mar-2014 |
wenzelm <none@none> |
proper configuration option "ML_print_depth"; proper ML_exception_trace for HOL-TPTP;
|
#
a38b5b7f |
|
16-Feb-2014 |
haftmann <none@none> |
eliminated odd dislocation of keyword declaration and implementation (leftover from 318cd8ac1817) --HG-- extra : rebase_source : cd1363dc0bc2ce86b25312caa19c52553840acd6
|
#
2fdeffeb |
|
30-Jan-2014 |
blanchet <none@none> |
added 'algebra' and 'meson' to 'try0'
|
#
6d11884a |
|
18-Oct-2013 |
blanchet <none@none> |
killed more "no_atp"s
|
#
68670fb3 |
|
12-Jul-2013 |
wenzelm <none@none> |
hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
|
#
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"
|
#
870593bf |
|
15-Mar-2012 |
wenzelm <none@none> |
declare command keywords via theory header, including strict checking outside Pure;
|
#
5e2ce29b |
|
24-Feb-2012 |
blanchet <none@none> |
renamed 'try_methods' to 'try0' --HG-- rename : src/HOL/Tools/try_methods.ML => src/HOL/Tools/try0.ML
|
#
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
|
#
5c3f2ec6 |
|
15-Nov-2011 |
blanchet <none@none> |
continued implementation of lambda-lifting in Metis
|
#
79752fb0 |
|
02-Sep-2011 |
blanchet <none@none> |
renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy) --HG-- rename : src/HOL/Tools/Metis/metis_tactics.ML => src/HOL/Tools/Metis/metis_tactic.ML
|
#
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
|
#
6eacd39e |
|
27-May-2011 |
blanchet <none@none> |
renamed "try" "try_methods" --HG-- rename : src/HOL/Tools/try.ML => src/HOL/Tools/try_methods.ML
|
#
247df2ed |
|
02-May-2011 |
wenzelm <none@none> |
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory; proper name bindings;
|
#
a9461bd5 |
|
14-Apr-2011 |
blanchet <none@none> |
make 48170228f562 work also with "HO_Reas" examples
|
#
6521a000 |
|
15-Dec-2010 |
blanchet <none@none> |
added Sledgehammer support for higher-order propositional reasoning
|
#
5580ed1a |
|
07-Dec-2010 |
blanchet <none@none> |
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer --HG-- rename : src/HOL/Tools/async_manager.ML => src/HOL/Tools/Sledgehammer/async_manager.ML
|
#
9fb7cd64 |
|
11-Oct-2010 |
blanchet <none@none> |
"setup" in theory
|
#
5e394636 |
|
04-Oct-2010 |
blanchet <none@none> |
hide one more name
|
#
c0d2d7bf |
|
05-Oct-2010 |
blanchet <none@none> |
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
|
#
e8c452f8 |
|
04-Oct-2010 |
blanchet <none@none> |
tuning
|
#
37d247fe |
|
04-Oct-2010 |
blanchet <none@none> |
move Metis into Plain --HG-- rename : src/HOL/Tools/Sledgehammer/metis_reconstruct.ML => src/HOL/Tools/Metis/metis_reconstruct.ML rename : src/HOL/Tools/Sledgehammer/metis_tactics.ML => src/HOL/Tools/Metis/metis_tactics.ML rename : src/HOL/Tools/Sledgehammer/metis_translate.ML => src/HOL/Tools/Metis/metis_translate.ML
|
#
cd8e9c18 |
|
20-Jun-2007 |
wenzelm <none@none> |
obsolete (cf. ATP_Linkup.thy);
|
#
89e1d065 |
|
20-Jun-2007 |
wenzelm <none@none> |
The Metis prover (slightly modified version from Larry);
|