Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -100 -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/ATP/atp_problem.ML
Thu, 09 Feb 2012 14:04:17 +0100 blanchet improved KBO weights -- beware of explicit applications file | diff | annotate
Thu, 09 Feb 2012 12:57:59 +0100 blanchet added possibility of generating KBO weights to DFG problems file | diff | annotate
Sat, 04 Feb 2012 12:08:18 +0100 blanchet improved hashing w.r.t. Mirabelle, to help debugging file | diff | annotate
Sat, 04 Feb 2012 12:08:18 +0100 blanchet tuned SPASS DFG output file | diff | annotate
Fri, 03 Feb 2012 18:00:55 +0100 blanchet extended SPASS/DFG output with ranks file | diff | annotate
Thu, 02 Feb 2012 01:55:17 +0100 blanchet tuning file | diff | annotate
Wed, 01 Feb 2012 17:16:55 +0100 blanchet really fixed syntax bug in DFG output (cf. ef62c2fafa9e) file | diff | annotate
Tue, 31 Jan 2012 15:13:18 +0100 blanchet avoid name clash, really file | diff | annotate
Tue, 31 Jan 2012 15:10:03 +0100 blanchet fixed syntax bug in DFG output file | diff | annotate
Tue, 31 Jan 2012 14:39:21 +0100 blanchet new SPASS setup file | diff | annotate
Tue, 31 Jan 2012 12:43:48 +0100 blanchet distinguish between ":lr" and ":lt" (terminating) in DFG format file | diff | annotate
Tue, 31 Jan 2012 10:29:05 +0100 blanchet nicer keyword class avoidance scheme file | diff | annotate
Thu, 26 Jan 2012 20:49:54 +0100 blanchet better handling of individual type for DFG format (SPASS) file | diff | annotate
Mon, 23 Jan 2012 17:40:32 +0100 blanchet renamed two files to make room for a new file file | diff | annotate
Tue, 20 Dec 2011 18:59:50 +0100 blanchet don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers file | diff | annotate
Tue, 20 Dec 2011 18:59:50 +0100 blanchet one more SPASS identifier file | diff | annotate
Tue, 13 Dec 2011 14:55:42 +0100 blanchet correctly declare implicit TFF1 types that appear first as type arguments with "$tType" and not "$i file | diff | annotate
Sat, 29 Oct 2011 13:15:58 +0200 blanchet always use DFG format to talk to SPASS -- since that's what we'll need to use anyway to benefit from sorts and other extensions file | diff | annotate
Sat, 29 Oct 2011 13:15:58 +0200 blanchet added DFG unsorted support (like in the old days) file | diff | annotate
Sat, 29 Oct 2011 13:15:58 +0200 blanchet added sorted DFG output for coming version of SPASS file | diff | annotate
Wed, 07 Sep 2011 13:50:17 +0200 blanchet fixed THF type constructor syntax file | diff | annotate
Tue, 06 Sep 2011 18:13:36 +0200 blanchet added dummy polymorphic THF system file | diff | annotate
Tue, 06 Sep 2011 09:11:08 +0200 blanchet tuning file | diff | annotate
Fri, 02 Sep 2011 14:43:20 +0200 blanchet use new syntax for Pi binder in TFF1 output file | diff | annotate
Wed, 31 Aug 2011 08:49:10 +0200 blanchet fixed explicit declaration of TFF1 types file | diff | annotate
Tue, 30 Aug 2011 16:07:46 +0200 blanchet generate properly typed TFF1 (PFF) problems in the presence of type class predicates file | diff | annotate
Tue, 30 Aug 2011 16:07:45 +0200 blanchet added type abstractions (for declaring polymorphic constants) to TFF syntax file | diff | annotate
Tue, 30 Aug 2011 16:07:45 +0200 blanchet implement more of the polymorphic simply typed format TFF(1) file | diff | annotate
Tue, 30 Aug 2011 16:07:34 +0200 blanchet first step towards polymorphic TFF + changed defaults for Vampire file | diff | annotate
Thu, 25 Aug 2011 23:38:09 +0200 blanchet make polymorphic encodings more complete file | diff | annotate
Thu, 25 Aug 2011 22:05:18 +0200 blanchet make TFF output less explicit where possible file | diff | annotate
Thu, 25 Aug 2011 13:55:52 +0100 nik added choice operator output for file | diff | annotate
Mon, 22 Aug 2011 15:02:45 +0200 blanchet tuning ATP problem output file | diff | annotate
Mon, 22 Aug 2011 15:02:45 +0200 blanchet clearer terminology file | diff | annotate
Wed, 17 Aug 2011 10:03:58 +0200 blanchet distinguish THF syntax with and without choice (Satallax vs. LEO-II) file | diff | annotate
Tue, 26 Jul 2011 14:53:00 +0200 blanchet further worked around LEO-II parser limitation, with eta-expansion file | diff | annotate
Tue, 26 Jul 2011 14:53:00 +0200 blanchet use syntactic sugar whenever possible in THF problems, to work around current LEO-II parser limitation (bang bang and query query are not handled correctly) file | diff | annotate
Thu, 14 Jul 2011 16:50:05 +0200 blanchet added option to control which lambda translation to use (for experiments) file | diff | annotate
Thu, 14 Jul 2011 15:14:38 +0200 blanchet don't generate Waldmeister problems with only a conjecture, since it makes it crash sometimes file | diff | annotate
Wed, 06 Jul 2011 17:19:34 +0100 blanchet make SML/NJ happy + tuning file | diff | annotate
Tue, 05 Jul 2011 17:09:59 +0100 nik improved translation of lambdas in THF file | diff | annotate
Tue, 05 Jul 2011 17:09:59 +0100 nik added generation of lambdas in THF file | diff | annotate
Tue, 05 Jul 2011 17:09:59 +0100 nik add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order) file | diff | annotate
Thu, 16 Jun 2011 13:50:35 +0200 blanchet added missing case in pattern matching -- solves Waldmeister "Match" exceptions that have been plaguing some users file | diff | annotate
Wed, 08 Jun 2011 16:20:19 +0200 blanchet pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types file | diff | annotate
Tue, 07 Jun 2011 07:06:24 +0200 blanchet renamed ML function file | diff | annotate
Mon, 06 Jun 2011 20:36:35 +0200 blanchet improved ATP clausifier so it can deal with "x => (y <=> z)" file | diff | annotate
Mon, 06 Jun 2011 20:36:34 +0200 blanchet killed odd connectives file | diff | annotate
Wed, 01 Jun 2011 10:29:43 +0200 blanchet clausify "<=>" (needed for some type information) file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet proper handling of type variable classes in new Metis file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet more work on new metis that exploits the powerful new type encodings file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet first step in sharing more code between ATP and Metis translation file | diff | annotate
Fri, 27 May 2011 10:30:07 +0200 blanchet cleaner handling of equality and proxies (esp. for THF) file | diff | annotate
Fri, 27 May 2011 10:30:07 +0200 blanchet fully support all type system encodings in typed formats (TFF, THF) file | diff | annotate
Fri, 27 May 2011 10:30:07 +0200 blanchet towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments) file | diff | annotate
Tue, 24 May 2011 18:04:23 +0200 blanchet ensure that the argument of logical negation is enclosed in parentheses in THF mode file | diff | annotate
Tue, 24 May 2011 10:01:03 +0200 blanchet more work on parsing LEO-II proofs and extracting uses of extensionality file | diff | annotate
Tue, 24 May 2011 10:01:00 +0200 blanchet tuning file | diff | annotate
Tue, 24 May 2011 10:00:38 +0200 blanchet more work on parsing LEO-II proofs without lambdas file | diff | annotate
Tue, 24 May 2011 00:01:33 +0200 blanchet identify HOL functions with THF functions file | diff | annotate
less more (0) -100 -60 tip
isabelle