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_Manager/atp_wrapper.ML
Thu, 22 Apr 2010 10:13:02 +0200 blanchet postprocess ATP output in "overlord" mode to make it more readable file | diff | annotate
Wed, 21 Apr 2010 17:06:26 +0200 blanchet failure of reconstructing the Isar proof (e.g., exception) should not prevent Sledgehammer from showing the short one-liner proof -- but in "debug" mode we do want to know what the exception is file | diff | annotate
Wed, 21 Apr 2010 16:38:03 +0200 blanchet generate command-line in addition to timestamp in ATP output file, for debugging purposes file | diff | annotate
Wed, 21 Apr 2010 16:21:19 +0200 blanchet pass relevant options from "sledgehammer" to "sledgehammer minimize"; file | diff | annotate
Wed, 21 Apr 2010 12:22:04 +0200 blanchet distinguish between the different ATP errors in the user interface; file | diff | annotate
Wed, 21 Apr 2010 11:03:35 +0200 blanchet added "spass_tptp" prover, which requires SPASS x.y > 3.0; file | diff | annotate
Tue, 20 Apr 2010 16:04:36 +0200 blanchet added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable) file | diff | annotate
Mon, 19 Apr 2010 18:44:12 +0200 blanchet get rid of "conjecture_pos", which is no longer necessary now that it's Metis's job, not Sledgehammer's, to report inconsistent contexts file | diff | annotate
Mon, 19 Apr 2010 15:15:21 +0200 blanchet make Sledgehammer's minimizer also minimize Isar proofs file | diff | annotate
Mon, 19 Apr 2010 11:54:07 +0200 blanchet don't use readable names if proof reconstruction is needed, because it uses the structure of names file | diff | annotate
Mon, 19 Apr 2010 10:45:08 +0200 blanchet rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does file | diff | annotate
Mon, 19 Apr 2010 10:15:02 +0200 blanchet set SPASS option on the command-line, so that it doesn't vanish when moving to TPTP format file | diff | annotate
Sat, 17 Apr 2010 10:42:09 +0200 blanchet added missing \n in output file | diff | annotate
Fri, 16 Apr 2010 20:50:50 +0200 blanchet added timestamp to proof file | diff | annotate
Fri, 16 Apr 2010 14:48:34 +0200 blanchet store nonmangled names along with mangled type names in Sledgehammer for debugging purposes file | diff | annotate
Thu, 15 Apr 2010 13:49:46 +0200 blanchet make Sledgehammer's output more debugging friendly file | diff | annotate
Wed, 14 Apr 2010 21:22:13 +0200 blanchet added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture file | diff | annotate
Wed, 14 Apr 2010 18:23:51 +0200 blanchet make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second file | diff | annotate
Mon, 29 Mar 2010 19:49:57 +0200 blanchet added "modulus" and "sorts" options to control Sledgehammer's Isar proof output file | diff | annotate
Mon, 29 Mar 2010 12:21:51 +0200 blanchet made "theory_const" a Sledgehammer option; file | diff | annotate
Mon, 29 Mar 2010 12:01:00 +0200 blanchet added "respect_no_atp" and "convergence" options to Sledgehammer; file | diff | annotate
Sun, 28 Mar 2010 16:59:06 +0200 wenzelm static defaults for configuration options; file | diff | annotate
Wed, 24 Mar 2010 14:49:32 +0100 blanchet added support for Sledgehammer parameters; file | diff | annotate
Mon, 22 Mar 2010 10:25:07 +0100 blanchet start work on direct proof reconstruction for Sledgehammer file | diff | annotate
Fri, 19 Mar 2010 16:04:15 +0100 blanchet renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar"; file | diff | annotate
Fri, 19 Mar 2010 15:33:18 +0100 blanchet move all ATP setup code into ATP_Wrapper file | diff | annotate
Fri, 19 Mar 2010 13:02:18 +0100 blanchet more Sledgehammer refactoring file | diff | annotate
Wed, 17 Mar 2010 19:26:05 +0100 blanchet renamed Sledgehammer structures file | diff | annotate
Thu, 04 Mar 2010 22:48:16 +0100 wenzelm basic simplification of external_prover signature; file | diff | annotate
Sat, 06 Feb 2010 14:50:55 +0100 wenzelm renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh; file | diff | annotate
Thu, 29 Oct 2009 16:59:12 +0100 wenzelm modernized some structure names; file | diff | annotate
Tue, 27 Oct 2009 18:00:50 +0100 boehmes measure runtime of ATPs only if requested file | diff | annotate
Fri, 23 Oct 2009 14:22:36 +0200 boehmes ignore error messages produced by ATPs file | diff | annotate
Thu, 15 Oct 2009 17:49:30 +0200 wenzelm natural argument order for prover; file | diff | annotate
Thu, 15 Oct 2009 15:53:33 +0200 wenzelm clarified File.platform_path vs. File.shell_path; file | diff | annotate
Thu, 15 Oct 2009 12:23:24 +0200 wenzelm misc tuning and recovery of Isabelle coding style; file | diff | annotate
Thu, 15 Oct 2009 11:49:27 +0200 wenzelm eliminated extraneous wrapping of public records; file | diff | annotate
Wed, 14 Oct 2009 23:44:37 +0200 wenzelm modernized structure names; file | diff | annotate
Sun, 04 Oct 2009 12:59:22 +0200 boehmes recovered support for Spass: re-enabled writing problems in DFG format file | diff | annotate
Sat, 03 Oct 2009 12:05:40 +0200 boehmes re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values, file | diff | annotate
Tue, 29 Sep 2009 16:24:36 +0200 wenzelm explicit indication of Unsynchronized.ref; file | diff | annotate
Thu, 17 Sep 2009 11:57:36 +0200 boehmes undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time"; file | diff | annotate
Tue, 15 Sep 2009 15:29:11 +0200 boehmes added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling); file | diff | annotate
Thu, 03 Sep 2009 17:55:31 +0200 boehmes added runtime information to sledgehammer file | diff | annotate
Mon, 31 Aug 2009 15:29:26 +0200 boehmes sledgehammer's temporary files are removed properly (even in case of an exception occurs) file | diff | annotate
Sat, 29 Aug 2009 21:57:06 +0200 boehmes propagate theorem names, in addition to generated return message file | diff | annotate
Tue, 04 Aug 2009 19:20:24 +0200 wenzelm src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place; file | diff | annotate | base
less more (0) tip
isabelle