2013-05-30 wenzelm 2013-05-30 standardized aliases;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-01-03 blanchet 2013-01-03 tuned comment
2013-01-03 blanchet 2013-01-03 avoid explosion in higher-order unification algorithm
2012-05-22 blanchet 2012-05-22 don't apply "ext_cong_neq" to biimplications
2012-05-22 blanchet 2012-05-22 make higher-order goals more first-order via extensionality
2012-05-22 blanchet 2012-05-22 added "ext_cong_neq" lemma (not used yet); tuning
2012-03-20 blanchet 2012-03-20 tuning
2012-03-19 wenzelm 2012-03-19 moved some legacy stuff;
2012-03-13 wenzelm 2012-03-13 prefer abs_def over def_raw;
2012-03-04 blanchet 2012-03-04 ensure no abstractions leak through after lambda-lifting (for formulas with higher-order occurrences of quantifiers)
2012-02-16 wenzelm 2012-02-16 explicit is better than implicit;
2012-01-03 blanchet 2012-01-03 tuning
2012-01-02 blanchet 2012-01-02 killed unfold_set_const option that makes no sense now that set is a type constructor again
2011-12-24 haftmann 2011-12-24 dropped references to obsolete facts `mem_def_raw` and `Collect_def_raw`
2011-12-02 wenzelm 2011-12-02 more antiquotations;
2011-11-18 blanchet 2011-11-18 avoid that var names get changed by resolution in Metis lambda-lifting
2011-07-25 blanchet 2011-07-25 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
2011-07-14 blanchet 2011-07-14 always unfold "Let"s is Sledgehammer, Metis, and MESON
2011-06-08 blanchet 2011-06-08 don't needlessly presimplify -- makes ATP problem preparation much faster
2011-05-17 blanchet 2011-05-17 use antiquotation
2011-05-13 wenzelm 2011-05-13 proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
2011-05-12 blanchet 2011-05-12 another concession to backward compatibility
2011-05-12 blanchet 2011-05-12 ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
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-02 wenzelm 2011-05-02 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory; proper name bindings;
2011-04-22 wenzelm 2011-04-22 modernized Quantifier1 simproc setup;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-14 blanchet 2011-04-14 remove experimental code added in 85bb6fbb8e6a
2011-04-14 blanchet 2011-04-14 experiment with definitional CNF
2010-11-26 blanchet 2010-11-26 renamed "trace_me{son,tis}" and "verbose_metis" to have the name of the tool first
2010-10-29 blanchet 2010-10-29 ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
2010-10-11 blanchet 2010-10-11 added "trace_meson" configuration option, replacing old-fashioned reference
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 got rid of overkill "meson_choice" attribute; tuning
2010-10-04 blanchet 2010-10-04 move Meson to Plain
2010-10-04 blanchet 2010-10-04 move MESON files together