src/HOL/Metis.thy
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-05-13 blanchet 2014-05-13 hide more internal names
2014-03-25 wenzelm 2014-03-25 proper configuration option "ML_print_depth"; proper ML_exception_trace for HOL-TPTP;
2014-02-16 haftmann 2014-02-16 eliminated odd dislocation of keyword declaration and implementation (leftover from 318cd8ac1817)
2014-01-30 blanchet 2014-01-30 added 'algebra' and 'meson' to 'try0'
2013-10-18 blanchet 2013-10-18 killed more "no_atp"s
2013-07-13 wenzelm 2013-07-13 hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-05-21 blanchet 2012-05-21 add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
2012-03-15 wenzelm 2012-03-15 declare command keywords via theory header, including strict checking outside Pure;
2012-02-24 blanchet 2012-02-24 renamed 'try_methods' to 'try0'
2012-01-23 blanchet 2012-01-23 renamed two files to make room for a new file
2011-11-15 blanchet 2011-11-15 continued implementation of lambda-lifting in Metis
2011-09-02 blanchet 2011-09-02 renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
2011-05-31 blanchet 2011-05-31 first step in sharing more code between ATP and Metis translation
2011-05-27 blanchet 2011-05-27 renamed "try" "try_methods"
2011-05-02 wenzelm 2011-05-02 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory; proper name bindings;
2011-04-14 blanchet 2011-04-14 make 48170228f562 work also with "HO_Reas" examples
2010-12-15 blanchet 2010-12-15 added Sledgehammer support for higher-order propositional reasoning
2010-12-07 blanchet 2010-12-07 load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
2010-10-11 blanchet 2010-10-11 "setup" in theory
2010-10-05 blanchet 2010-10-05 hide one more name
2010-10-05 blanchet 2010-10-05 hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
2010-10-04 blanchet 2010-10-04 tuning
2010-10-04 blanchet 2010-10-04 move Metis into Plain
2007-06-20 wenzelm 2007-06-20 The Metis prover (slightly modified version from Larry);