src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
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