2010-06-25 blanchet 2010-06-25 more moving around of ML files in "Sledgehammer.thy"
2010-06-25 blanchet 2010-06-25 got rid of needless exception
2010-06-25 blanchet 2010-06-25 further reduce dependencies on "sledgehammer_fact_filter.ML"
2010-06-24 blanchet 2010-06-24 a76ace919f1c wasn't quite right; second try
2010-06-24 blanchet 2010-06-24 never include anything from the Sledgehammer theory in the relevant facts + killed two obsolete facts
2010-06-24 blanchet 2010-06-24 better eta-expansion in Sledgehammer's clausification; make the eta-expansion code more robust in the face of polymorphic arguments + make eta-expansion happen more often, since it first-orderizes things
2010-06-23 blanchet 2010-06-23 use Skolem inlining also in the nonpolymorphic case, as a step toward simplifying the source code
2010-06-23 blanchet 2010-06-23 this looks like the most appropriate place to do the beta-eta-contraction
2010-06-23 blanchet 2010-06-23 killed legacy "neg_clausify" and "clausify"
2010-06-22 blanchet 2010-06-22 thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
2010-06-22 blanchet 2010-06-22 removed Sledgehammer's support for the DFG syntax; this removes 350 buggy lines from Sledgehammer. SPASS 3.5 and above support the TPTP syntax.
2010-06-22 blanchet 2010-06-22 reintroduce new Sledgehammer polymorphic handling code; this time I tested the proper version of Isabelle
2010-06-22 blanchet 2010-06-22 reredisable new polymorphic code
2010-06-21 blanchet 2010-06-21 beta-eta was too much, because it transformed SOME x. P x into Eps P, which caused problems later; reintroduced old proof based on Metis, since it was a good test for the Skolemizer
2010-06-15 blanchet 2010-06-15 found missing beta-eta-contraction
2010-06-14 blanchet 2010-06-14 turn off new polymorphism code again -- a new issue popped up
2010-06-14 blanchet 2010-06-14 no point in introducing combinators for inlined Skolem functions
2010-06-14 blanchet 2010-06-14 adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
2010-06-12 blanchet 2010-06-12 disable new polymorphic code for now, until remaining issues in "equality_inf" are resolved
2010-06-11 blanchet 2010-06-11 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
2010-06-07 blanchet 2010-06-07 cosmetics
2010-06-05 blanchet 2010-06-05 renaming
2010-06-05 blanchet 2010-06-05 show more respect for user-specified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
2010-06-05 blanchet 2010-06-05 make Sledgehammer's "add:" and "del:" syntax work better in the presence of aliases; some of these aliases pop up only after Sledgehammer has converted the formula to CNF, so it can be very confusing to the user who said "add: foo del: bar" that "bar" is used in the end.
2010-06-04 blanchet 2010-06-04 don't raise Option.Option if assumptions contain schematic variables
2010-05-28 blanchet 2010-05-28 make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2010-04-30 wenzelm 2010-04-30 renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;
2010-04-28 blanchet 2010-04-28 save the name of Skolemized variables in Sledgehammer for use in the proof reconstruction code
2010-04-27 blanchet 2010-04-27 fix types of "fix" variables to help proof reconstruction and aid readability
2010-04-26 blanchet 2010-04-26 make "neg_clausify" return a list of lists of clauses, so that it's possible to see which clause comes from which theorem
2010-04-25 blanchet 2010-04-25 move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
2010-04-25 blanchet 2010-04-25 support readable names even when Isar proof reconstruction is enabled -- useful for debugging
2010-04-19 blanchet 2010-04-19 got rid of somewhat pointless "pairname" function in Sledgehammer
2010-04-11 wenzelm 2010-04-11 Thm.add_axiom/add_def: return internal name of foundational axiom;
2010-03-27 wenzelm 2010-03-27 eliminated old-style Theory.add_defs_i;
2010-03-25 blanchet 2010-03-25 make Mirabelle happy again
2010-03-23 blanchet 2010-03-23 added options to Sledgehammer; syntax: sledgehammer [options] goal_no, where "[options]" and "goal_no" are optional
2010-03-22 blanchet 2010-03-22 merged
2010-03-22 blanchet 2010-03-22 start work on direct proof reconstruction for Sledgehammer
2010-03-19 blanchet 2010-03-19 more Sledgehammer refactoring
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-18 blanchet 2010-03-18 now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
2010-03-17 blanchet 2010-03-17 renamed Sledgehammer structures
2010-03-17 blanchet 2010-03-17 move Sledgehammer files in a directory of their own