src/HOL/Tools/ATP/reduce_axiomsN.ML
2006-10-04 haftmann 2006-10-04 insert replacing ins ins_int ins_string
2006-10-02 paulson 2006-10-02 Changing the default for theory_const
2006-09-18 paulson 2006-09-18 Added the max_new parameter, which is a cap on how many clauses may be admitted per round. Also various tidying up.
2006-09-13 paulson 2006-09-13 Added the "theory_const" option. Only it is OFF because it's often harmful!
2006-09-01 paulson 2006-09-01 refinements to conversion into clause form, esp for the HO case
2006-08-28 paulson 2006-08-28 minor bug fixes
2006-07-25 wenzelm 2006-07-25 use Term.add_vars instead of obsolete term_varnames;
2006-07-19 paulson 2006-07-19 Fixed the bugs introduced by the last commit! Output is now *identical* to that produced by the old version, based on a-lists.
2006-07-15 paulson 2006-07-15 Replaced a-lists by tables to improve efficiency
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.