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/ATP/atp_problem.ML
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
Tue, 24 May 2011 00:01:33 +0200 blanchet started adding support for THF output (but no lambdas) file | diff | annotate
Tue, 24 May 2011 00:01:33 +0200 blanchet eliminated more code duplication in Nitrox file | diff | annotate
Sun, 22 May 2011 14:51:42 +0200 blanchet improved Waldmeister support -- even run it by default on unit equational goals file | diff | annotate
Sun, 22 May 2011 14:51:04 +0200 blanchet removed SNARK hack now that SNARK is fixed file | diff | annotate
Sun, 22 May 2011 14:51:01 +0200 blanchet added support for remote Waldmeister file | diff | annotate
Sun, 22 May 2011 14:49:35 +0200 blanchet reorganized ATP formats a little bit file | diff | annotate
Thu, 12 May 2011 15:29:19 +0200 blanchet fixed several bugs in Isar proof reconstruction, in particular w.r.t. mangled types and hAPP file | diff | annotate
Thu, 12 May 2011 15:29:19 +0200 blanchet tuning file | diff | annotate
Thu, 12 May 2011 15:29:18 +0200 blanchet added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option file | diff | annotate
Thu, 12 May 2011 15:29:18 +0200 blanchet renamed type systems for more consistency file | diff | annotate
Fri, 06 May 2011 13:34:59 +0200 blanchet allow each prover to specify its own formula kind for symbols occurring in the conjecture file | diff | annotate
Tue, 03 May 2011 18:47:22 +0200 blanchet fixed long name truncation logic file | diff | annotate
Mon, 02 May 2011 22:52:15 +0200 blanchet SNARK workaround file | diff | annotate
Mon, 02 May 2011 22:52:15 +0200 blanchet proper default for TPTP source filed file | diff | annotate
Sun, 01 May 2011 18:37:25 +0200 blanchet restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags" file | diff | annotate
Sun, 01 May 2011 18:37:25 +0200 blanchet avoid trailing digits for SNARK (type) names -- grr... file | diff | annotate
Sun, 01 May 2011 18:37:25 +0200 blanchet made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet shorten readable names -- they can get really long with monomorphization, which actually slows down the ATPs file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet declare TFF types so that SNARK can be used with types file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet generate pure TFF problems -- ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas) file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet generate TFF type declarations in typed mode file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet added more rudimentary type support to Sledgehammer's ATP encoding file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet fixed type of ATP quantifier types (sic) file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet added "useful_info" argument to ATP formulas -- this will probably be useful later to specify intro, simp, elim to SPASS file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet added support for TFF type declarations file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet reintroduced constructor for formulas, and automatically detect which logic to use (TFF or FOF) to avoid clutter file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet added room for types in ATP quantifiers file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet distinguish FOF and TFF (typed first-order) in ATP abstract syntax tree file | diff | annotate
Thu, 21 Apr 2011 22:18:28 +0200 blanchet detect some unsound proofs before showing them to the user file | diff | annotate
Mon, 04 Apr 2011 18:53:35 +0200 blanchet if "monomorphize" is enabled, mangle the type information in the names by default file | diff | annotate
Fri, 18 Feb 2011 12:32:55 +0100 blanchet extended ATP problem syntax to support other applications than Sledgehammer, e.g. experiments with ATPs file | diff | annotate
Mon, 10 Jan 2011 15:45:46 +0100 wenzelm eliminated Int.toString; file | diff | annotate
Thu, 16 Sep 2010 11:59:45 +0200 blanchet use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs file | diff | annotate
Thu, 16 Sep 2010 11:12:08 +0200 blanchet factored out TSTP/SPASS/Vampire proof parsing; file | diff | annotate
Wed, 15 Sep 2010 10:26:09 +0200 blanchet in debug mode, don't touch "$true" and "$false" file | diff | annotate
Thu, 02 Sep 2010 22:49:56 +0200 blanchet fix bug in "debug" mode file | diff | annotate
Sun, 22 Aug 2010 09:43:10 +0200 blanchet prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible; file | diff | annotate
Fri, 20 Aug 2010 15:16:27 +0200 blanchet use "hypothesis" rather than "conjecture" for hypotheses in TPTP format; file | diff | annotate
Tue, 17 Aug 2010 16:46:43 +0200 blanchet more parentheses in TPTP formulas, just in case file | diff | annotate
Thu, 29 Jul 2010 16:11:02 +0200 blanchet fix bug with "=" vs. "fequal" introduced by last change (dddb8ba3a1ce) file | diff | annotate
Wed, 28 Jul 2010 19:04:59 +0200 blanchet consequence of directory renaming file | diff | annotate
Wed, 28 Jul 2010 19:01:34 +0200 blanchet rename directory file | diff | annotate | base
less more (0) tip
isabelle