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
2010-10-04 blanchet 2010-10-04 move MESON files together