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);