Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
early warning when Sledgehammer finds a proof
|
file |
diff |
annotate
|
Sat, 05 Mar 2016 17:01:45 +0100 |
wenzelm |
tuned signature -- clarified modules;
|
file |
diff |
annotate
|
Thu, 03 Mar 2016 15:23:02 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Mon, 01 Feb 2016 19:57:58 +0100 |
blanchet |
preplaying of 'smt' and 'metis' more in sync with actual method
|
file |
diff |
annotate
|
Mon, 05 Oct 2015 23:03:50 +0200 |
blanchet |
further improved fine point w.r.t. replaying in the presence of chained facts and a non-empty meta-quantifier prefix + avoid printing internal names in backquotes
|
file |
diff |
annotate
|
Fri, 02 Oct 2015 21:15:25 +0200 |
blanchet |
further reduced dependency on legacy async thread manager
|
file |
diff |
annotate
|
Fri, 02 Oct 2015 21:06:32 +0200 |
blanchet |
removed legacy asynchronous mode in Sledgehammer
|
file |
diff |
annotate
|
Mon, 21 Sep 2015 23:22:11 +0200 |
wenzelm |
clarified markup;
|
file |
diff |
annotate
|
Mon, 29 Jun 2015 23:44:53 +0200 |
blanchet |
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
|
file |
diff |
annotate
|
Mon, 22 Jun 2015 16:56:03 +0200 |
blanchet |
keep 'Pure.all' in goals when preplaying
|
file |
diff |
annotate
|
Mon, 22 Jun 2015 16:56:03 +0200 |
blanchet |
use right context for preplay, to avoid errors in fact lookup
|
file |
diff |
annotate
|
Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
Thu, 29 Jan 2015 16:35:29 +0100 |
wenzelm |
more explicit indication of Async_Manager_Legacy as Proof General legacy;
|
file |
diff |
annotate
|
Tue, 23 Dec 2014 20:46:42 +0100 |
wenzelm |
explicit message channels for "state", "information";
|
file |
diff |
annotate
|
Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
Fri, 07 Nov 2014 16:36:55 +0100 |
wenzelm |
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
|
file |
diff |
annotate
|
Thu, 06 Nov 2014 13:36:19 +0100 |
wenzelm |
prefer explicit Keyword.keywords;
|
file |
diff |
annotate
|
Mon, 03 Nov 2014 14:31:15 +0100 |
wenzelm |
eliminated obsolete Proof.goal_message -- print outcome more directly;
|
file |
diff |
annotate
|
Fri, 31 Oct 2014 11:36:41 +0100 |
wenzelm |
discontinued obsolete Output.urgent_message;
|
file |
diff |
annotate
|
Tue, 30 Sep 2014 16:40:03 +0200 |
blanchet |
don't call 'hd' on a possibly empty list
|
file |
diff |
annotate
|
Mon, 04 Aug 2014 13:06:24 +0200 |
blanchet |
default on 'metis' for ATPs if preplaying is disabled
|
file |
diff |
annotate
|
Mon, 04 Aug 2014 12:52:48 +0200 |
blanchet |
more informative preplay failures
|
file |
diff |
annotate
|
Mon, 04 Aug 2014 12:28:42 +0200 |
blanchet |
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
|
file |
diff |
annotate
|
Mon, 04 Aug 2014 11:43:19 +0200 |
blanchet |
honor 'dont_minimize' option when preplaying one-liner proof
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
export ML function
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
restored a bit of laziness
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
further minimize one-liner
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
eliminated needlessly complex message tail
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
rationalized preplaying by eliminating (now superfluous) laziness
|
file |
diff |
annotate
|
Tue, 15 Jul 2014 00:21:32 +0200 |
blanchet |
record MaSh algorithm in spying data
|
file |
diff |
annotate
|
Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
tuned message
|
file |
diff |
annotate
|
Thu, 26 Jun 2014 20:32:31 +0200 |
blanchet |
reintroduced MaSh hints, this time as persistent creatures
|
file |
diff |
annotate
|
Thu, 26 Jun 2014 18:57:20 +0200 |
blanchet |
tuned output
|
file |
diff |
annotate
|
Thu, 26 Jun 2014 13:35:39 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Mon, 16 Jun 2014 19:40:04 +0200 |
blanchet |
moved code around
|
file |
diff |
annotate
|
Wed, 28 May 2014 12:34:26 +0200 |
blanchet |
optimized computation
|
file |
diff |
annotate
|
Thu, 22 May 2014 05:23:50 +0200 |
blanchet |
properly reconstruct helpers in Z3 proofs
|
file |
diff |
annotate
|
Thu, 22 May 2014 03:29:35 +0200 |
blanchet |
shorten Sledgehammer output, as suggested by Andrei Popescu
|
file |
diff |
annotate
|
Wed, 21 May 2014 14:09:42 +0200 |
blanchet |
avoid markup-generating @{make_string}
|
file |
diff |
annotate
|
Thu, 27 Mar 2014 17:12:40 +0100 |
wenzelm |
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
|
file |
diff |
annotate
|
Thu, 13 Feb 2014 13:16:17 +0100 |
blanchet |
avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures
|
file |
diff |
annotate
|
Mon, 03 Feb 2014 16:53:58 +0100 |
blanchet |
renamed ML file
|
file |
diff |
annotate
|
Mon, 03 Feb 2014 15:33:18 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
Fri, 31 Jan 2014 16:10:39 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
Fri, 31 Jan 2014 10:23:32 +0100 |
blanchet |
renamed many Sledgehammer ML files to clarify structure
|
file |
diff |
annotate
| base
|
Tue, 07 Dec 2010 16:27:07 +0100 |
blanchet |
pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
|
file |
diff |
annotate
|
Tue, 07 Dec 2010 14:53:12 +0100 |
boehmes |
centralized handling of built-in types and constants;
|
file |
diff |
annotate
|
Mon, 06 Dec 2010 11:41:24 +0100 |
blanchet |
handle "max_relevant" uniformly
|
file |
diff |
annotate
|
Mon, 06 Dec 2010 11:26:17 +0100 |
blanchet |
honor the default max relevant facts setting from the SMT solvers in Sledgehammer
|
file |
diff |
annotate
|
Mon, 06 Dec 2010 10:31:29 +0100 |
blanchet |
trust SMT filter's timeout -- nested timeouts seem to be at the origin of spontaneous Interrupt exceptions in some cases
|
file |
diff |
annotate
|
Mon, 06 Dec 2010 10:23:31 +0100 |
blanchet |
reraise interrupt exceptions
|
file |
diff |
annotate
|
Fri, 03 Dec 2010 18:29:14 +0100 |
blanchet |
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
|
file |
diff |
annotate
|
Fri, 26 Nov 2010 22:22:07 +0100 |
blanchet |
put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs
|
file |
diff |
annotate
|
Fri, 26 Nov 2010 09:15:49 +0100 |
blanchet |
adjust Sledgehammer/SMT fudge factor
|
file |
diff |
annotate
|
Thu, 25 Nov 2010 14:58:50 +0100 |
blanchet |
cosmetics
|
file |
diff |
annotate
|
Thu, 25 Nov 2010 13:26:12 +0100 |
blanchet |
set Metis option on correct context, lest it be ignored
|
file |
diff |
annotate
|
Thu, 25 Nov 2010 12:11:12 +0100 |
blanchet |
make "debug" mode of Sledgehammer/SMT more liberal
|
file |
diff |
annotate
|
Wed, 24 Nov 2010 16:15:15 +0100 |
blanchet |
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
|
file |
diff |
annotate
|