src/HOL/Tools/res_clause.ML
2007-08-17 wenzelm 2007-08-17 proper signature; removed unused const_types_of;
2007-08-08 paulson 2007-08-08 Code to undo the function ascii_of
2007-07-20 haftmann 2007-07-20 moved class ord from Orderings.thy to HOL.thy
2007-06-14 paulson 2007-06-14 Deleted unused code
2007-05-22 paulson 2007-05-22 Some hacks for SPASS format
2007-05-19 haftmann 2007-05-19 constant op @ now named append
2007-05-17 haftmann 2007-05-17 canonical prefixing of class constants
2007-04-12 paulson 2007-04-12 Improved and simplified the treatment of classrel/arity clauses
2007-03-02 paulson 2007-03-02 Meson.is_fol_term now takes a theory as argument. Minor tidying.
2007-01-20 wenzelm 2007-01-20 Output.debug: non-strict; renamed Output.show_debug_msgs to Output.debugging (coincides with Toplevel.debug);
2007-01-17 paulson 2007-01-17 Deleted mk_fol_type, since the constructors can be used directly
2006-12-15 wenzelm 2006-12-15 avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-12-13 paulson 2006-12-13 Deleted the unused type argument of UVar
2006-12-12 paulson 2006-12-12 Removal of the "keep_types" flag: we always keep types!
2006-11-27 mengj 2006-11-27 Added in another function clause_name_of.
2006-11-27 paulson 2006-11-27 tidied code
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.