src/HOL/Tools/Metis/metis_reconstruct.ML
2011-04-14 blanchet 2011-04-14 "unify_first_prem_with_concl" (cf. 9ceb585c097a) sometimes throws an exception, but it is very rarely needed -- catch the exception for now
2011-04-14 blanchet 2011-04-14 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
2011-04-14 blanchet 2011-04-14 removed obsolete Skolem counter in new Skolemizer
2011-04-14 blanchet 2011-04-14 use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
2011-04-14 blanchet 2011-04-14 make new Skolemizer work also for "metisFT"
2011-04-14 blanchet 2011-04-14 try to repair out-of-sync situations in Metis
2011-04-07 blanchet 2011-04-07 further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
2011-04-07 blanchet 2011-04-07 make new Skolemizer more robust
2011-03-24 blanchet 2011-03-24 clean up new Skolemizer code -- some old hacks are no longer necessary
2011-03-24 blanchet 2011-03-24 remove newly added wrong logic
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-01-10 wenzelm 2011-01-10 eliminated Int.toString;
2010-12-15 blanchet 2010-12-15 remove at most one double negation -- any other double negations are part of some higher-order reasoning and should be left alone, cf. "HO_Reas.thy"
2010-12-15 blanchet 2010-12-15 added Sledgehammer support for higher-order propositional reasoning
2010-12-15 blanchet 2010-12-15 add Metis support for higher-order propositional reasoning
2010-12-15 blanchet 2010-12-15 tuning: unused var
2010-12-02 blanchet 2010-12-02 give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
2010-11-26 blanchet 2010-11-26 renamed "trace_me{son,tis}" and "verbose_metis" to have the name of the tool first
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 fixed order of quantifier instantiation in new Skolemizer
2010-10-29 blanchet 2010-10-29 more work on new Skolemizer without Hilbert_Choice
2010-10-29 blanchet 2010-10-29 prevent type errors because of inconsistent skolem Var types by giving fresh indices to Skolems
2010-10-29 blanchet 2010-10-29 make handling of parameters more robust, by querying the goal
2010-10-27 blanchet 2010-10-27 do not let Metis be confused by higher-order reasoning leading to literals of the form "~ ~ p", which are really the same as "p"
2010-10-26 blanchet 2010-10-26 clearer error messages
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-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-04 blanchet 2010-10-04 move Metis into Plain