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
2005-07-11 quigley 2005-07-11 Fixed some problems with the signal handler.
2005-07-07 paulson 2005-07-07 inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
2005-06-03 paulson 2005-06-03 no longer emits literals for type class HOL.type; also minor tidying
2005-05-23 quigley 2005-05-23 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML. Changed watcher.ML so that the Unix.execute and Unix.reap functions are used instead of those in modUnix.ML, and consequently removed modUnix.ML from Reconstruction.thy
2005-05-12 paulson 2005-05-12 theorem names for caching
2005-04-19 paulson 2005-04-19 more tidying of libraries in Reconstruction
2005-03-22 paulson 2005-03-22 ensuring that "equal" is not a function
2005-03-15 paulson 2005-03-15 more concise ASCII escaping
2005-03-14 paulson 2005-03-14 bug fixes involving typechecking clauses
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-01-21 paulson 2005-01-21 Jia Meng: delta simpsets and clasets
2004-12-09 paulson 2004-12-09 Comments and other tweaks by Jia
2004-11-30 paulson 2004-11-30 resolution package tools by Jia Meng