src/HOL/Tools/res_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-21 paulson 2006-11-21 Optimized class_pairs for the common case of no subclasses
2006-11-18 haftmann 2006-11-18 dvd_def now with object equality
2006-11-15 paulson 2006-11-15 Arity clauses are now produced only for types and type classes actually used.
2006-11-10 paulson 2006-11-10 Improvement to classrel clauses: now outputs the minimum needed. Theorem names: trying to minimize the number of multiple theorem names presented
2006-11-08 wenzelm 2006-11-08 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
2006-10-04 haftmann 2006-10-04 insert replacing ins ins_int ins_string
2006-10-02 paulson 2006-10-02 extensions for Susanto
2006-09-30 mengj 2006-09-30 Added the combinator constants to the constants table.
2006-08-28 paulson 2006-08-28 removed the (apparently pointless) signature constraint
2006-08-25 paulson 2006-08-25 tidied
2006-07-07 paulson 2006-07-07 Some tidying. Fixed a problem where the DFG file did not declare some TFrees as 0-ary functions. Frees no longer have types attached.
2006-07-06 paulson 2006-07-06 some tidying; fixed the output of theorem names
2006-07-05 paulson 2006-07-05 removed the "tagging" feature
2006-07-05 mengj 2006-07-05 Literals aren't sorted any more. Output overloaded constants' type var instantiations.
2006-05-25 mengj 2006-05-25 Changed input interface of dfg_write_file.
2006-05-16 wenzelm 2006-05-16 more abstract interface to classes/arities;
2006-05-01 wenzelm 2006-05-01 adapted arities;
2006-04-19 paulson 2006-04-19 the "th" field of type "clause"
2006-04-18 mengj 2006-04-18 Take conjectures and axioms as thms when convert them to ResClause.clause format.
2006-04-07 mengj 2006-04-07 tptp_write_file accepts axioms as thm.
2006-03-17 haftmann 2006-03-17 renamed op < <= to Orderings.less(_eq)
2006-03-10 haftmann 2006-03-10 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
2006-03-07 paulson 2006-03-07 Tidying and tracing. Handling exn CLAUSE so that errors don't reach top-level.
2006-03-07 mengj 2006-03-07 tptp_write_file now takes goals and axioms as Term.term and writes them to a file.
2006-03-02 paulson 2006-03-02 reformatting
2006-02-28 paulson 2006-02-28 new order for arity clauses
2006-02-03 paulson 2006-02-03 removal of case analysis clauses
2006-01-31 paulson 2006-01-31 removal of ResClause.num_of_clauses and other simplifications
2006-01-31 paulson 2006-01-31 working SPASS support; much tidying
2006-01-31 paulson 2006-01-31 reorganization of code to support DFG otuput
2006-01-30 paulson 2006-01-30 tidy-up of res_clause.ML, removing the "predicates" field
2006-01-27 paulson 2006-01-27 tidying up SPASS output
2006-01-13 paulson 2006-01-13 more readable divide ops
2005-12-21 paulson 2005-12-21 new hash table module in HOL/Too/s
2005-12-20 mengj 2005-12-20 Added functions for fol_type; also put some functions to the signature, used by ResHolClause.
2005-12-16 paulson 2005-12-16 hashing to eliminate the output of duplicate clauses
2005-12-15 paulson 2005-12-15 No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are deleted; any positive occurrence of HOL.type kills the entire clause.
2005-12-15 mengj 2005-12-15 Added functions to test equivalence between clauses.
2005-12-14 mengj 2005-12-14 Changed literals' ordering and the functions for sorting literals.
2005-12-14 mengj 2005-12-14 1. changed fol_type, it's not a string type anymore. 2. sort literals in clauses.
2005-12-13 paulson 2005-12-13 now generates the name "append"
2005-11-28 mengj 2005-11-28 Only output types if !keep_types is true.
2005-11-22 paulson 2005-11-22 new treatment of polymorphic types, using Sign.const_typargs
2005-11-18 mengj 2005-11-18 -- before converting axiom and conjecture clauses into ResClause.clause format, perform "check_is_fol_term" first.
2005-11-02 wenzelm 2005-11-02 Sign.const_monomorphic;
2005-10-28 mengj 2005-10-28 Added several functions to the signature. Added two new functions, which are used by res_hol_clause.ML programs.
2005-10-27 wenzelm 2005-10-27 replaced Defs.monomorphic by Sign.monomorphic;
2005-10-19 mengj 2005-10-19 More functions are added to the signature of ResClause
2005-10-18 paulson 2005-10-18 new interface to make_conjecture_clauses
2005-10-14 paulson 2005-10-14 deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
2005-10-07 paulson 2005-10-07 minor code tidyig
2005-10-05 paulson 2005-10-05 improved process handling. tidied
2005-10-04 paulson 2005-10-04 reset clause counter
2005-09-20 paulson 2005-09-20 tidying, and support for axclass/classrel clauses
2005-09-15 paulson 2005-09-15 massive tidy-up and simplification
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-15 paulson 2005-09-15 the experimental tagging system, and the usual tidying
2005-09-14 paulson 2005-09-14 nice names for more infix operators