src/HOL/Tools/ATP/reduce_axiomsN.ML
2006-04-19 paulson 2006-04-19 definition expansion checks for excess variables
2006-04-07 mengj 2006-04-07 filter now accepts axioms as thm, instead of term.
2006-04-05 paulson 2006-04-05 pool of constants; definition expansion; current best settings
2006-03-31 paulson 2006-03-31 Removal of unused code
2006-03-28 paulson 2006-03-28 Simplified version of Jia's filter. Now all constants are pooled, rather than relevance being compared against separate clauses. Rejects are no longer noted, and units cannot be added at the end.
2006-03-23 paulson 2006-03-23 detection of definitions of relevant constants
2006-03-22 paulson 2006-03-22 Removal of obsolete strategies. Initial support for locales: Frees and Consts treated similarly.
2006-03-10 paulson 2006-03-10 Frequency analysis of constants (with types). Ability to restrict the number of accepted clauses.
2006-03-08 paulson 2006-03-08 Frequency strategy. Revised indentation, etc.
2006-03-07 paulson 2006-03-07 Tidying and restructuring.
2006-03-07 mengj 2006-03-07 relevance_filter takes input axioms as Term.term.
2006-02-13 mengj 2006-02-13 Fixed a bug of type unification.
2006-02-11 mengj 2006-02-11 Added another filter strategy.
2006-01-27 mengj 2006-01-27 Relevance filtering. Has replaced the previous version.