2015-07-27 wenzelm 2015-07-27 tuned signature;
2015-07-25 wenzelm 2015-07-25 updated to infer_instantiate; tuned;
2015-07-05 wenzelm 2015-07-05 simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
2015-06-01 wenzelm 2015-06-01 clarified context;
2015-03-06 wenzelm 2015-03-06 clarified context;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 wenzelm 2015-03-04 clarified signature;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-12-21 wenzelm 2014-12-21 proper context;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-07-01 blanchet 2014-07-01 use context instead of theory
2014-05-01 haftmann 2014-05-01 optional case enforcement
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-02-16 blanchet 2014-02-16 removed final periods in messages for proof methods
2014-02-01 wenzelm 2014-02-01 more standard file/module names;
2014-02-01 wenzelm 2014-02-01 proper context for printing;
2013-12-31 wenzelm 2013-12-31 proper context for norm_hhf and derived operations; clarified tool context in some boundary cases;
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-05-16 blanchet 2013-05-16 tuning -- renamed '_from_' to '_of_' in Sledgehammer
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-01-03 blanchet 2013-01-03 use new skolemizer for reconstructing skolemization steps in Isar proofs (because the old skolemizer messes up the order of the Skolem arguments)
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-13 wenzelm 2012-03-13 prefer abs_def over def_raw;
2012-02-15 wenzelm 2012-02-15 renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
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-02 wenzelm 2011-12-02 more antiquotations;
2011-11-15 blanchet 2011-11-15 continued implementation of lambda-lifting in Metis
2011-11-15 blanchet 2011-11-15 started implementing lambda-lifting in Metis
2011-08-17 wenzelm 2011-08-17 modernized signature of Term.absfree/absdummy; eliminated obsolete Term.list_abs_free;
2011-08-10 wenzelm 2011-08-10 old term operations are legacy;
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-06-09 wenzelm 2011-06-09 discontinued Name.variant to emphasize that this is old-style / indirect;
2011-05-22 blanchet 2011-05-22 improved Waldmeister support -- even run it by default on unit equational goals
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-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-14 blanchet 2011-04-14 remove needless export
2011-04-14 blanchet 2011-04-14 properly implemented definitional CNF for the new Skolemizer (and moved the code for the old Skolemizer -- tuning), removing big chunks for experimental/debugging code
2011-04-14 blanchet 2011-04-14 improve definitional CNF on goal by moving "not" past the quantifiers
2011-04-14 blanchet 2011-04-14 experiment with definitional CNF
2011-04-14 blanchet 2011-04-14 try to repair out-of-sync situations in Metis
2011-04-07 blanchet 2011-04-07 tuned comment
2011-03-26 wenzelm 2011-03-26 merged
2011-03-24 blanchet 2011-03-24 avoid evil "export_without_context", which breaks if there are local "fixes"
2011-03-24 blanchet 2011-03-24 more robust handling of variables in new Skolemizer
2011-03-24 wenzelm 2011-03-24 added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
2011-03-23 blanchet 2011-03-23 avoid illegal variable names, which then yield "Not an identifier" errors in "rename_tac"
2010-12-17 wenzelm 2010-12-17 refer to regular structure Simplifier;
2010-10-29 blanchet 2010-10-29 restructure Skolemization code slightly
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 more work on new Skolemizer without Hilbert_Choice
2010-10-29 blanchet 2010-10-29 fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
2010-10-06 blanchet 2010-10-06 qualify "Meson." and "Metis." constants so that the ML files can be reloaded later (e.g. for testing/development)
2010-10-05 blanchet 2010-10-05 got rid of overkill "meson_choice" attribute; tuning
2010-10-05 blanchet 2010-10-05 more explicit name
2010-10-05 blanchet 2010-10-05 factor out "Meson_Tactic" from "Meson_Clausify"
2010-10-04 blanchet 2010-10-04 move Meson to Plain