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_manager.ML
Sun, 25 Apr 2010 10:22:31 +0200 blanchet cosmetics: rename internal functions file | diff | annotate
Sat, 24 Apr 2010 16:05:42 +0200 blanchet better error reporting; file | diff | annotate
Fri, 23 Apr 2010 19:16:52 +0200 blanchet make "ATP_Manager.get_prover" a total function, since we always want to show the same error text file | diff | annotate
Fri, 23 Apr 2010 16:55:51 +0200 blanchet move some sledgehammer stuff out of "atp_manager.ML" file | diff | annotate
Fri, 23 Apr 2010 16:21:47 +0200 blanchet give an error if no ATP is set file | diff | annotate
Fri, 23 Apr 2010 16:15:35 +0200 blanchet move the Sledgehammer menu options to "sledgehammer_isar.ML" file | diff | annotate
Fri, 23 Apr 2010 15:48:34 +0200 blanchet centralized ATP-specific error handling in "atp_wrapper.ML" file | diff | annotate
Fri, 23 Apr 2010 13:16:50 +0200 blanchet handle ATP proof delimiters in a cleaner, more extensible fashion file | diff | annotate
Fri, 23 Apr 2010 16:12:57 +0200 bulwahn initialized atps reference with standard setup in the atp manager file | diff | annotate
Thu, 22 Apr 2010 16:30:04 +0200 blanchet set "atps" reference's default value to "(remote_)e (remote_)spass (remote_)vampire", based on what is installed file | diff | annotate
Wed, 21 Apr 2010 16:21:19 +0200 blanchet pass relevant options from "sledgehammer" to "sledgehammer minimize"; 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 17:18:21 +0200 blanchet workaround for Proof General's off-by-a-few sendback display bug, whereby "pr" in "proof" is not highlighted file | diff | annotate
Mon, 19 Apr 2010 16:29:52 +0200 blanchet cosmetics 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 10:45:08 +0200 blanchet rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does file | diff | annotate
Fri, 16 Apr 2010 16:51:54 +0200 blanchet output total time taken by Sledgehammer if "verbose" is set file | diff | annotate
Fri, 16 Apr 2010 15:59:53 +0200 blanchet tell the user that Sledgehammer kills its siblings 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
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 18:44:24 +0200 blanchet make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer" 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
Wed, 24 Mar 2010 14:49:32 +0100 blanchet added support for Sledgehammer parameters; 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 15:07:44 +0100 blanchet move the Sledgehammer Isar commands together into one file; 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
Fri, 05 Mar 2010 23:51:32 +0100 wenzelm use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing; file | diff | annotate
Thu, 04 Mar 2010 22:46:07 +0100 wenzelm tuned; file | diff | annotate
Tue, 10 Nov 2009 23:18:03 +0100 wenzelm Toplevel.thread provides Isar-style exception output; file | diff | annotate
Sun, 08 Nov 2009 18:43:42 +0100 wenzelm adapted Theory_Data; file | diff | annotate
Thu, 29 Oct 2009 16:59:12 +0100 wenzelm modernized some structure names; file | diff | annotate
Thu, 29 Oct 2009 16:09:16 +0100 wenzelm unregister: eliminated unused status; file | diff | annotate
Wed, 28 Oct 2009 22:18:00 +0100 wenzelm renamed raw Proof.get_goal to Proof.raw_goal; file | diff | annotate
Tue, 27 Oct 2009 11:25:56 +0100 wenzelm SimpleThread.fork: uniform handling of outermost Interrupt, which is not an error and should not produce exception trace; file | diff | annotate
Sun, 18 Oct 2009 22:16:37 +0200 wenzelm removed disjunctive group cancellation -- provers run independently; file | diff | annotate
Sun, 18 Oct 2009 21:13:29 +0200 wenzelm tuned; file | diff | annotate
Fri, 16 Oct 2009 00:26:19 +0200 wenzelm made SML/NJ happy; file | diff | annotate
Thu, 15 Oct 2009 17:49:30 +0200 wenzelm natural argument order for prover; file | diff | annotate
Thu, 15 Oct 2009 17:06:19 +0200 wenzelm ATP_Manager.get_prover: canonical argument order; file | diff | annotate
Thu, 15 Oct 2009 11:49:27 +0200 wenzelm eliminated extraneous wrapping of public records; file | diff | annotate
Thu, 15 Oct 2009 11:12:09 +0200 wenzelm renamed functor HeapFun to Heap; file | diff | annotate
Thu, 15 Oct 2009 10:59:10 +0200 wenzelm misc tuning and clarification; file | diff | annotate
Thu, 15 Oct 2009 00:55:29 +0200 wenzelm structure ATP_Manager: eliminated slightly odd get/set operations in favour of Unsynchronized.ref; file | diff | annotate
Wed, 14 Oct 2009 23:44:37 +0200 wenzelm modernized structure names; file | diff | annotate
Sat, 03 Oct 2009 12:10:16 +0200 boehmes merged 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
Fri, 02 Oct 2009 23:15:36 +0200 wenzelm eliminated dead code; file | diff | annotate
Thu, 01 Oct 2009 16:46:48 +0200 nipkow made spass additional default prover file | diff | annotate
Tue, 29 Sep 2009 16:24:36 +0200 wenzelm explicit indication of Unsynchronized.ref; file | diff | annotate
Thu, 03 Sep 2009 17:55:31 +0200 boehmes added runtime information to sledgehammer 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