src/HOL/Tools/res_hol_clause.ML
2006-11-24 paulson 2006-11-24 ATP linkup now generates "new TPTP" rather than "old TPTP"
2006-11-22 paulson 2006-11-22 Consolidation of code to "blacklist" unhelpful theorems, including record surjectivity properties
2006-11-16 paulson 2006-11-16 Includes type:sort constraints in its code to collect predicates in axiom clauses.
2006-11-08 wenzelm 2006-11-08 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
2006-11-01 paulson 2006-11-01 Numerous cosmetic changes. Use of ---> notation for types. Added rules for the introduction of the iff connective, but they are too prolific to be useful.
2006-10-30 paulson 2006-10-30 Purely cosmetic
2006-10-12 paulson 2006-10-12 Extended combinators now disabled
2006-10-10 paulson 2006-10-10 Combinators require the theory name; added settings for SPASS
2006-10-05 mengj 2006-10-05 Changed and removed some functions related to combinators, since they are Isabelle constants now.
2006-10-05 paulson 2006-10-05 Now the DFG output includes correct declarations of c_fequal, but not hEXTENT
2006-09-30 mengj 2006-09-30 Combinator axioms are now from Isabelle theorems, no need to use helper files. Removed LAM2COMB exception.
2006-09-21 paulson 2006-09-21 corrected for the translation from _ to __ in c_COMBx_e
2006-09-20 mengj 2006-09-20 Introduced combinators B', C' and S'.
2006-08-28 paulson 2006-08-28 tidied
2006-08-08 paulson 2006-08-08 tidying
2006-08-02 mengj 2006-08-02 Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
2006-08-01 mengj 2006-08-01 Added in code to check too general axiom clauses.
2006-07-15 mengj 2006-07-15 Only include combinators if required by goals and user specified lemmas. Remove a clause if too general.
2006-07-13 paulson 2006-07-13 "conjecture" must be lower case
2006-07-06 paulson 2006-07-06 some tidying; fixed the output of theorem names
2006-07-05 mengj 2006-07-05 Literals aren't sorted any more.
2006-06-29 paulson 2006-06-29 added the "th" field to datatype Clause
2006-05-29 paulson 2006-05-29 warnings to debug outputs; default translation to const-typed
2006-05-25 mengj 2006-05-25 Changed the DFG format's functions' declaration procedure.
2006-05-25 mengj 2006-05-25 Fixed a bug.
2006-05-25 mengj 2006-05-25 HOL problems now have DFG output format.
2006-04-28 mengj 2006-04-28 changed the functions for getting HOL helper clauses.
2006-04-22 mengj 2006-04-22 Changed the treatment of equalities.
2006-04-18 mengj 2006-04-18 Take conjectures and axioms as thms when convert them to ResHolClause.clause format.
2006-04-07 mengj 2006-04-07 tptp_write_file accepts axioms as thm.
2006-03-07 mengj 2006-03-07 Added tptp_write_file to write all necessary ATP input clauses to one file.
2006-02-23 mengj 2006-02-23 Default type level is T_FULL now.
2006-01-30 paulson 2006-01-30 tidy-up of res_clause.ML, removing the "predicates" field
2006-01-20 mengj 2006-01-20 fixed a bug
2005-12-21 paulson 2005-12-21 new hash table module in HOL/Too/s
2005-12-20 mengj 2005-12-20 Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
2005-12-06 mengj 2005-12-06 Added new type embedding methods for translating HOL clauses.
2005-11-28 mengj 2005-11-28 Added flags for setting and detecting whether a problem needs combinators.
2005-11-18 mengj 2005-11-18 -- terms are fully typed. -- only the top-level boolean terms are predicates.
2005-10-28 mengj 2005-10-28 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.