src/HOL/Tools/res_clause.ML
2006-10-04 ago insert replacing ins ins_int ins_string
2006-10-02 ago extensions for Susanto
2006-09-30 ago Added the combinator constants to the constants table.
2006-08-28 ago removed the (apparently pointless) signature constraint
2006-08-25 ago tidied
2006-07-07 ago Some tidying.
2006-07-06 ago some tidying; fixed the output of theorem names
2006-07-05 ago removed the "tagging" feature
2006-07-05 ago Literals aren't sorted any more. Output overloaded constants' type var instantiations.
2006-05-25 ago Changed input interface of dfg_write_file.
2006-05-16 ago more abstract interface to classes/arities;
2006-05-01 ago adapted arities;
2006-04-19 ago the "th" field of type "clause"
2006-04-18 ago Take conjectures and axioms as thms when convert them to ResClause.clause format.
2006-04-07 ago tptp_write_file accepts axioms as thm.
2006-03-17 ago renamed op < <= to Orderings.less(_eq)
2006-03-10 ago renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
2006-03-07 ago Tidying and tracing. Handling exn CLAUSE so that errors don't reach top-level.
2006-03-07 ago tptp_write_file now takes goals and axioms as Term.term and writes them to a file.
2006-03-02 ago reformatting
2006-02-28 ago new order for arity clauses
2006-02-03 ago removal of case analysis clauses
2006-01-31 ago removal of ResClause.num_of_clauses and other simplifications
2006-01-31 ago working SPASS support; much tidying
2006-01-31 ago reorganization of code to support DFG otuput
2006-01-30 ago tidy-up of res_clause.ML, removing the "predicates" field
2006-01-27 ago tidying up SPASS output
2006-01-13 ago more readable divide ops
2005-12-21 ago new hash table module in HOL/Too/s
2005-12-20 ago Added functions for fol_type; also put some functions to the signature, used by ResHolClause.
2005-12-16 ago hashing to eliminate the output of duplicate clauses
2005-12-15 ago No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
2005-12-15 ago Added functions to test equivalence between clauses.
2005-12-14 ago Changed literals' ordering and the functions for sorting literals.
2005-12-14 ago 1. changed fol_type, it's not a string type anymore.
2005-12-13 ago now generates the name "append"
2005-11-28 ago Only output types if !keep_types is true.
2005-11-22 ago new treatment of polymorphic types, using Sign.const_typargs
2005-11-18 ago -- before converting axiom and conjecture clauses into ResClause.clause format, perform "check_is_fol_term" first.
2005-11-02 ago Sign.const_monomorphic;
2005-10-28 ago Added several functions to the signature.
2005-10-27 ago replaced Defs.monomorphic by Sign.monomorphic;
2005-10-19 ago More functions are added to the signature of ResClause
2005-10-18 ago new interface to make_conjecture_clauses
2005-10-14 ago deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
2005-10-07 ago minor code tidyig
2005-10-05 ago improved process handling. tidied
2005-10-04 ago reset clause counter
2005-09-20 ago tidying, and support for axclass/classrel clauses
2005-09-15 ago massive tidy-up and simplification
2005-09-15 ago TableFun/Symtab: curried lookup and update;
2005-09-15 ago the experimental tagging system, and the usual tidying
2005-09-14 ago nice names for more infix operators
2005-09-09 ago Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
2005-09-08 ago yet more tidying of Isabelle-ATP link
2005-09-07 ago axioms now included in tptp files, no /bin/cat and various tidying
2005-09-05 ago curried_lookup/update;
2005-09-02 ago further tidying up of Isabelle-ATP link
2005-09-02 ago fixed arities and restored changes that had gone missing
2005-08-26 ago DFG output now works for untyped rules (ML "ResClause.untyped();")