src/HOL/Tools/res_hol_clause.ML
2009-06-03 immler 2009-06-03 split preparing clauses and writing problemfile; included results of count_constants in return-type of prover; optionally pass counted constants to prover; removed unused external_prover from signature
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2009-02-27 wenzelm 2009-02-27 turned "read-only refs" typ_level and minimize_applies into constant values;
2009-02-26 immler 2009-02-26 removed global ref dfg_format
2009-02-25 immler 2009-02-25 removed local ref const_needs_hBOOL; renamed some const_min_arity parameters to cma
2009-02-24 immler 2009-02-24 removed local ref const_min_arity
2008-11-18 wenzelm 2008-11-18 changes by Fabian Immler: improved handling of prover errors; explicit treatment of clauses that are too trivial for resolution;
2008-06-12 wenzelm 2008-06-12 use regular error function;
2008-06-12 wenzelm 2008-06-12 ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
2007-10-30 paulson 2007-10-30 bugfixes concerning strange theorems
2007-10-12 paulson 2007-10-12 preventing eta-redexes in theorems from causing failure
2007-10-10 paulson 2007-10-10 removed dead code
2007-10-10 paulson 2007-10-10 getting rid of type typ_var
2007-10-09 paulson 2007-10-09 context-based treatment of generalization; also handling TFrees in axiom clauses
2007-08-21 paulson 2007-08-21 Deleted the partially-typed translation and the combinator code. Minimize_applies now uses the same translation code, which handles both cases anyway.
2007-08-18 wenzelm 2007-08-18 removed stateful init: operations take proper theory argument;
2007-08-17 wenzelm 2007-08-17 proper signature;
2007-08-10 paulson 2007-08-10 removal of some refs
2007-06-14 paulson 2007-06-14 Now also handles FO problems
2007-05-07 paulson 2007-05-07 First-order variant of the fully-typed translation
2007-04-30 paulson 2007-04-30 Fixing bugs in the partial-typed and fully-typed translations
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 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC minimize_applies is now by default TRUE!
2007-01-14 paulson 2007-01-14 optimized translation of HO problems
2006-12-15 wenzelm 2006-12-15 avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-12-01 paulson 2006-12-01 Deleted dead code
2006-11-28 paulson 2006-11-28 Removed the references for counting combinators. Instead they are counted in actual clauses.
2006-11-27 paulson 2006-11-27 Tidied code. Bool constructor is not needed.
2006-11-24 paulson 2006-11-24 Conversion of "equal" to "=" for TSTP format; big tidy-up
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-16 paulson 2006-11-16 Includes type:sort constraints in its code to collect predicates in axiom clauses.
2006-11-08 wenzelm 2006-11-08 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
2006-11-01 paulson 2006-11-01 Numerous cosmetic changes. Use of ---> notation for types. Added rules for the introduction of the iff connective, but they are too prolific to be useful.
2006-10-30 paulson 2006-10-30 Purely cosmetic
2006-10-12 paulson 2006-10-12 Extended combinators now disabled
2006-10-10 paulson 2006-10-10 Combinators require the theory name; added settings for SPASS
2006-10-05 mengj 2006-10-05 Changed and removed some functions related to combinators, since they are Isabelle constants now.
2006-10-05 paulson 2006-10-05 Now the DFG output includes correct declarations of c_fequal, but not hEXTENT
2006-09-30 mengj 2006-09-30 Combinator axioms are now from Isabelle theorems, no need to use helper files. Removed LAM2COMB exception.
2006-09-21 paulson 2006-09-21 corrected for the translation from _ to __ in c_COMBx_e
2006-09-20 mengj 2006-09-20 Introduced combinators B', C' and S'.
2006-08-28 paulson 2006-08-28 tidied
2006-08-08 paulson 2006-08-08 tidying
2006-08-02 mengj 2006-08-02 Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
2006-08-01 mengj 2006-08-01 Added in code to check too general axiom clauses.
2006-07-15 mengj 2006-07-15 Only include combinators if required by goals and user specified lemmas. Remove a clause if too general.
2006-07-13 paulson 2006-07-13 "conjecture" must be lower case
2006-07-06 paulson 2006-07-06 some tidying; fixed the output of theorem names
2006-07-05 mengj 2006-07-05 Literals aren't sorted any more.
2006-06-29 paulson 2006-06-29 added the "th" field to datatype Clause
2006-05-29 paulson 2006-05-29 warnings to debug outputs; default translation to const-typed
2006-05-25 mengj 2006-05-25 Changed the DFG format's functions' declaration procedure.
2006-05-25 mengj 2006-05-25 Fixed a bug.
2006-05-25 mengj 2006-05-25 HOL problems now have DFG output format.
2006-04-28 mengj 2006-04-28 changed the functions for getting HOL helper clauses.
2006-04-22 mengj 2006-04-22 Changed the treatment of equalities.
2006-04-18 mengj 2006-04-18 Take conjectures and axioms as thms when convert them to ResHolClause.clause format.