src/HOL/Tools/Metis/metis_tactics.ML
2011-05-12 blanchet 2011-05-12 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
2011-05-12 blanchet 2011-05-12 added unfold set constant functionality to Meson/Metis -- disabled by default for now
2011-05-12 blanchet 2011-05-12 more robust exception handling in Metis (also works if there are several subgoals)
2011-05-03 blanchet 2011-05-03 reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
2011-05-02 wenzelm 2011-05-02 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory; proper name bindings;
2011-05-01 blanchet 2011-05-01 added a hint to Metis errors suggesting metisFT -- it sometimes work
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-14 blanchet 2011-04-14 removed obsolete Skolem counter in new Skolemizer
2011-04-14 blanchet 2011-04-14 improve definitional CNF on goal by moving "not" past the quantifiers
2010-11-23 blanchet 2010-11-23 added "verbose" option to Metis to shut up its warnings if necessary
2010-10-29 blanchet 2010-10-29 ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
2010-10-29 blanchet 2010-10-29 prevent type errors because of inconsistent skolem Var types by giving fresh indices to Skolems
2010-10-26 blanchet 2010-10-26 renaming
2010-10-11 blanchet 2010-10-11 added "trace_meson" configuration option, replacing old-fashioned reference
2010-10-11 blanchet 2010-10-11 added "trace_metis" configuration option, replacing old-fashioned references
2010-10-06 blanchet 2010-10-06 move code from "Metis_Tactics" to "Metis_Reconstruct"
2010-10-06 blanchet 2010-10-06 get rid of function that duplicates existing Pure functionality
2010-10-06 blanchet 2010-10-06 added a few FIXMEs
2010-10-05 blanchet 2010-10-05 tuned comments
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-05 blanchet 2010-10-05 clean up debugging output
2010-10-05 blanchet 2010-10-05 got rid of overkill "meson_choice" attribute; tuning
2010-10-04 blanchet 2010-10-04 move Metis into Plain