History log of /seL4-l4v-master/isabelle/src/HOL/Metis.thy
Revision Date Author Comments
# 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);