src/HOL/Tools/res_clause.ML
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
2005-09-09 paulson 2005-09-09 Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
2005-09-08 paulson 2005-09-08 yet more tidying of Isabelle-ATP link
2005-09-07 paulson 2005-09-07 axioms now included in tptp files, no /bin/cat and various tidying
2005-09-05 wenzelm 2005-09-05 curried_lookup/update;
2005-09-02 paulson 2005-09-02 further tidying up of Isabelle-ATP link
2005-09-02 paulson 2005-09-02 fixed arities and restored changes that had gone missing
2005-08-26 quigley 2005-08-26 DFG output now works for untyped rules (ML "ResClause.untyped();")
2005-08-01 wenzelm 2005-08-01 Defs.monomorphic;
2005-07-28 paulson 2005-07-28 uniform treatment of variable prefixes
2005-07-27 paulson 2005-07-27 simpler variable names, and no types for monomorphic constants
2005-07-22 paulson 2005-07-22 streamlined the tptp output
2005-07-13 paulson 2005-07-13 tidied