Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/res_hol_clause.ML
Sat, 20 Jan 2007 14:09:14 +0100 wenzelm Output.debug: non-strict; file | diff | annotate
Wed, 17 Jan 2007 09:52:06 +0100 paulson Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC file | diff | annotate
Sun, 14 Jan 2007 09:57:29 +0100 paulson optimized translation of HO problems file | diff | annotate
Fri, 15 Dec 2006 00:08:06 +0100 wenzelm avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert; file | diff | annotate
Fri, 01 Dec 2006 12:23:53 +0100 paulson Deleted dead code file | diff | annotate
Tue, 28 Nov 2006 16:19:01 +0100 paulson Removed the references for counting combinators. Instead they are counted in actual clauses. file | diff | annotate
Mon, 27 Nov 2006 18:18:25 +0100 paulson Tidied code. Bool constructor is not needed. file | diff | annotate
Fri, 24 Nov 2006 16:38:42 +0100 paulson Conversion of "equal" to "=" for TSTP format; big tidy-up file | diff | annotate
Fri, 24 Nov 2006 13:24:30 +0100 paulson ATP linkup now generates "new TPTP" rather than "old TPTP" file | diff | annotate
Wed, 22 Nov 2006 20:08:07 +0100 paulson Consolidation of code to "blacklist" unhelpful theorems, including record file | diff | annotate
Thu, 16 Nov 2006 17:06:24 +0100 paulson Includes type:sort constraints in its code to collect predicates in axiom clauses. file | diff | annotate
Wed, 08 Nov 2006 21:45:15 +0100 wenzelm incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; file | diff | annotate
Wed, 01 Nov 2006 15:49:43 +0100 paulson Numerous cosmetic changes. file | diff | annotate
Mon, 30 Oct 2006 16:42:46 +0100 paulson Purely cosmetic file | diff | annotate
Thu, 12 Oct 2006 15:50:43 +0200 paulson Extended combinators now disabled file | diff | annotate
Tue, 10 Oct 2006 15:30:48 +0200 paulson Combinators require the theory name; added settings for SPASS file | diff | annotate
Thu, 05 Oct 2006 13:54:17 +0200 mengj Changed and removed some functions related to combinators, since they are Isabelle constants now. file | diff | annotate
Thu, 05 Oct 2006 10:46:26 +0200 paulson Now the DFG output includes correct declarations of c_fequal, but not hEXTENT file | diff | annotate
Sat, 30 Sep 2006 14:32:36 +0200 mengj Combinator axioms are now from Isabelle theorems, no need to use helper files. file | diff | annotate
Thu, 21 Sep 2006 17:31:10 +0200 paulson corrected for the translation from _ to __ in c_COMBx_e file | diff | annotate
Wed, 20 Sep 2006 13:54:03 +0200 mengj Introduced combinators B', C' and S'. file | diff | annotate
Mon, 28 Aug 2006 18:15:32 +0200 paulson tidied file | diff | annotate
Tue, 08 Aug 2006 18:40:04 +0200 paulson tidying file | diff | annotate
Wed, 02 Aug 2006 13:48:21 +0200 mengj Only ignore too general axiom clauses, if the translation is partial- or constant-typed. file | diff | annotate
Tue, 01 Aug 2006 13:44:05 +0200 mengj Added in code to check too general axiom clauses. file | diff | annotate
Sat, 15 Jul 2006 13:50:26 +0200 mengj Only include combinators if required by goals and user specified lemmas. file | diff | annotate
Thu, 13 Jul 2006 17:39:56 +0200 paulson "conjecture" must be lower case file | diff | annotate
Thu, 06 Jul 2006 12:18:17 +0200 paulson some tidying; fixed the output of theorem names file | diff | annotate
Wed, 05 Jul 2006 14:22:09 +0200 mengj Literals aren't sorted any more. file | diff | annotate
Thu, 29 Jun 2006 18:11:15 +0200 paulson added the "th" field to datatype Clause file | diff | annotate
Mon, 29 May 2006 17:38:02 +0200 paulson warnings to debug outputs; default translation to const-typed file | diff | annotate
Thu, 25 May 2006 14:08:55 +0200 mengj Changed the DFG format's functions' declaration procedure. file | diff | annotate
Thu, 25 May 2006 11:53:01 +0200 mengj Fixed a bug. file | diff | annotate
Thu, 25 May 2006 08:09:10 +0200 mengj HOL problems now have DFG output format. file | diff | annotate
Fri, 28 Apr 2006 05:59:32 +0200 mengj changed the functions for getting HOL helper clauses. file | diff | annotate
Sat, 22 Apr 2006 06:06:39 +0200 mengj Changed the treatment of equalities. file | diff | annotate
Tue, 18 Apr 2006 05:38:18 +0200 mengj Take conjectures and axioms as thms when convert them to ResHolClause.clause format. file | diff | annotate
Fri, 07 Apr 2006 05:12:51 +0200 mengj tptp_write_file accepts axioms as thm. file | diff | annotate
Tue, 07 Mar 2006 03:59:48 +0100 mengj Added tptp_write_file to write all necessary ATP input clauses to one file. file | diff | annotate
Thu, 23 Feb 2006 13:00:18 +0100 mengj Default type level is T_FULL now. file | diff | annotate
Mon, 30 Jan 2006 15:31:31 +0100 paulson tidy-up of res_clause.ML, removing the "predicates" field file | diff | annotate
Fri, 20 Jan 2006 04:35:23 +0100 mengj fixed a bug file | diff | annotate
Wed, 21 Dec 2005 12:06:08 +0100 paulson new hash table module in HOL/Too/s file | diff | annotate
Tue, 20 Dec 2005 04:29:25 +0100 mengj Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words. file | diff | annotate
Tue, 06 Dec 2005 06:21:07 +0100 mengj Added new type embedding methods for translating HOL clauses. file | diff | annotate
Mon, 28 Nov 2005 07:17:07 +0100 mengj Added flags for setting and detecting whether a problem needs combinators. file | diff | annotate
Fri, 18 Nov 2005 07:10:00 +0100 mengj -- terms are fully typed. file | diff | annotate
Fri, 28 Oct 2005 02:23:49 +0200 mengj A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format. file | diff | annotate
less more (0) tip
isabelle