src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
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-17 blanchet 2010-05-17 make sure chained facts don't pop up in the metis proof
2010-05-14 blanchet 2010-05-14 renamed two Sledgehammer options
2010-05-05 haftmann 2010-05-05 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-04-28 blanchet 2010-04-28 make sure short theorem names are preferred to composite ones in Sledgehammer; this code used to work at some point
2010-04-27 blanchet 2010-04-27 remove "higher_order" option from Sledgehammer -- the "smart" default is good enough
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 make Sledgehammer's "add:" and "del:" syntax really work (I hope), by comparing CNF theorems with CNF theorems
2010-04-19 blanchet 2010-04-19 rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
2010-04-16 blanchet 2010-04-16 optimize relevance filter by doing a Table.fold directly rather than destroying the datastructure each time; saves 2 sec per Sledgehammer invocation on my laptop!
2010-04-16 blanchet 2010-04-16 reorganize Sledgehammer's relevance filter slightly
2010-03-29 blanchet 2010-03-29 remove use of Polyhash; the new code is slightly faster. Also, "subtract_cls" now has canonical argument ordering.
2010-03-29 blanchet 2010-03-29 reintroduce efficient set structure to collect "no_atp" theorems
2010-03-29 blanchet 2010-03-29 made "theory_const" a Sledgehammer option; by default, it's true for SPASS and false for the others. This eliminates the need for the "spass_no_tc" ATP, which can be obtained by passing "no_theory_const" instead.
2010-03-29 blanchet 2010-03-29 added "respect_no_atp" and "convergence" options to Sledgehammer; these were previously hard-coded in "sledgehammer_fact_filter.ML"
2010-03-24 blanchet 2010-03-24 revert debugging output that shouldn't have been submitted in the first place
2010-03-24 blanchet 2010-03-24 honor the newly introduced Sledgehammer parameters and fixed the parsing; e.g. the prover "e_isar" (formely "e_full") is gone, instead do sledgehammer [atps = e, isar_proof] to get the same effect
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-19 blanchet 2010-03-19 more Sledgehammer refactoring
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