src/HOL/Tools/res_hol_clause.ML
2006-10-12 ago Extended combinators now disabled
2006-10-10 ago Combinators require the theory name; added settings for SPASS
2006-10-05 ago Changed and removed some functions related to combinators, since they are Isabelle constants now.
2006-10-05 ago Now the DFG output includes correct declarations of c_fequal, but not hEXTENT
2006-09-30 ago Combinator axioms are now from Isabelle theorems, no need to use helper files.
2006-09-21 ago corrected for the translation from _ to __ in c_COMBx_e
2006-09-20 ago Introduced combinators B', C' and S'.
2006-08-28 ago tidied
2006-08-08 ago tidying
2006-08-02 ago Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
2006-08-01 ago Added in code to check too general axiom clauses.
2006-07-15 ago Only include combinators if required by goals and user specified lemmas.
2006-07-13 ago "conjecture" must be lower case
2006-07-06 ago some tidying; fixed the output of theorem names
2006-07-05 ago Literals aren't sorted any more.
2006-06-29 ago added the "th" field to datatype Clause
2006-05-29 ago warnings to debug outputs; default translation to const-typed
2006-05-25 ago Changed the DFG format's functions' declaration procedure.
2006-05-25 ago Fixed a bug.
2006-05-25 ago HOL problems now have DFG output format.
2006-04-28 ago changed the functions for getting HOL helper clauses.
2006-04-22 ago Changed the treatment of equalities.
2006-04-18 ago Take conjectures and axioms as thms when convert them to ResHolClause.clause format.
2006-04-07 ago tptp_write_file accepts axioms as thm.
2006-03-07 ago Added tptp_write_file to write all necessary ATP input clauses to one file.
2006-02-23 ago Default type level is T_FULL now.
2006-01-30 ago tidy-up of res_clause.ML, removing the "predicates" field
2006-01-20 ago fixed a bug
2005-12-21 ago new hash table module in HOL/Too/s
2005-12-20 ago Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
2005-12-06 ago Added new type embedding methods for translating HOL clauses.
2005-11-28 ago Added flags for setting and detecting whether a problem needs combinators.
2005-11-18 ago -- terms are fully typed.
2005-10-28 ago 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.