| Tue, 28 Sep 2021 10:47:18 +0200 |
desharna |
prefer veriT over Z3 in sledgehammer
|
file |
diff |
annotate
|
| Tue, 28 Sep 2021 10:38:36 +0200 |
desharna |
added Zipperposition to sledgehammer's default provers
|
file |
diff |
annotate
|
| Wed, 22 Sep 2021 12:41:40 +0200 |
desharna |
removed checks for non-commercial usage of Vampire as it is now under BSD licence
|
file |
diff |
annotate
|
| Thu, 08 Jul 2021 17:23:01 +0200 |
desharna |
refactored Sledgehammer option "induction_rules"
|
file |
diff |
annotate
|
| Thu, 08 Jul 2021 15:25:30 +0200 |
desharna |
promoted "sledgehammer_instantiate_inducts" to proper option "induction_rules"
|
file |
diff |
annotate
|
| Fri, 14 May 2021 21:32:11 +0200 |
wenzelm |
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
|
file |
diff |
annotate
|
| Thu, 08 Oct 2020 17:02:56 +0200 |
desharna |
tune filename
|
file |
diff |
annotate
|
| Wed, 10 Jun 2020 15:55:41 +0200 |
blanchet |
simplified 'smt_proofs' option to be a binary option (instead of ternary), now that SMT proofs are accepted in the AFP (done with Martin Desharnais)
|
file |
diff |
annotate
|
| Fri, 25 Oct 2019 14:55:14 +0200 |
blanchet |
removed E-SInE, a very old system by now (and SInE has been incorporated in many provers in the past decade)
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Mon, 02 Jul 2018 10:02:44 +0200 |
blanchet |
added option for noncommercial Vampire
|
file |
diff |
annotate
|
| Thu, 11 Jan 2018 13:48:17 +0100 |
wenzelm |
uniform use of Standard ML op-infix -- eliminated warnings;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Wed, 23 Nov 2016 20:55:58 +0100 |
blanchet |
made MaSh faster and less likely to hang seemingly forever
|
file |
diff |
annotate
|
| Sun, 14 Aug 2016 12:26:09 +0200 |
blanchet |
killed final stops in Sledgehammer and friends
|
file |
diff |
annotate
|
| Tue, 24 May 2016 15:24:32 +0200 |
wenzelm |
clarified syntax categories;
|
file |
diff |
annotate
|
| Wed, 13 Apr 2016 18:01:05 +0200 |
wenzelm |
eliminated "xname" and variants;
|
file |
diff |
annotate
|
| Sat, 09 Apr 2016 14:17:50 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 12 Mar 2016 21:23:58 +0100 |
wenzelm |
create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
|
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
|
| Thu, 16 Jul 2015 17:47:49 +0200 |
blanchet |
keep smart default for Isar proofs in Sledgehammer panel (if the option is not checked)
|
file |
diff |
annotate
|
| Mon, 29 Jun 2015 20:55:46 +0200 |
wenzelm |
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
|
file |
diff |
annotate
|
| Thu, 25 Jun 2015 12:41:43 +0200 |
blanchet |
put E before (typically remote, hence less reliable) Vampire
|
file |
diff |
annotate
|
| Wed, 24 Jun 2015 00:30:03 +0200 |
blanchet |
silence 'try'
|
file |
diff |
annotate
|
| Thu, 28 May 2015 10:18:46 +0200 |
blanchet |
made Auto Sledgehammer behave more like the real thing
|
file |
diff |
annotate
|
| Fri, 08 May 2015 15:32:27 +0200 |
wenzelm |
sledgehammer panel operation re-uses more of the Isar command, notably Try0.silence_methods to avoid spurious warnings intruding the document view;
|
file |
diff |
annotate
|
| Fri, 08 May 2015 15:07:27 +0200 |
wenzelm |
more standard command setup;
|
file |
diff |
annotate
|
| Sat, 25 Apr 2015 20:49:26 +0200 |
wenzelm |
added checkbox for try0;
|
file |
diff |
annotate
|
| Wed, 22 Apr 2015 20:14:43 +0200 |
wenzelm |
allow diagnostic proof commands with skip_proofs;
|
file |
diff |
annotate
|
| Thu, 16 Apr 2015 14:18:32 +0200 |
wenzelm |
explicit error for Toplevel.proof_of;
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 18:55:52 +0200 |
blanchet |
reorder provers to reflect current eval results
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 17:06:48 +0200 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
| Wed, 11 Feb 2015 14:48:06 +0100 |
blanchet |
tuned default provers
|
file |
diff |
annotate
|
| Mon, 03 Nov 2014 14:50:27 +0100 |
wenzelm |
eliminated unused int_only flag (see also c12484a27367);
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 11:18:17 +0100 |
wenzelm |
discontinued Proof General;
|
file |
diff |
annotate
|
| Thu, 30 Oct 2014 11:08:26 +0100 |
wenzelm |
proper syntax categery "name" -- as usual and as documented;
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 20:05:39 +0200 |
blanchet |
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 16:58:27 +0200 |
blanchet |
going back to bc06471cb7b7 for silencing -- the bad side effects occurred only with 'smt', and the alternative silencing sometimes broke 'auto' etc.
|
file |
diff |
annotate
|
| Thu, 21 Aug 2014 22:48:39 +0200 |
wenzelm |
tuned signature -- define some elementary operations earlier;
|
file |
diff |
annotate
|
| Mon, 04 Aug 2014 15:02:02 +0200 |
blanchet |
cleaner 'compress' option
|
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 |
simplified minimization logic
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 23:52:56 +0200 |
blanchet |
always minimize Sledgehammer results by default
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 23:52:56 +0200 |
blanchet |
reduced preplay timeout to 1 s
|
file |
diff |
annotate
|
| Fri, 25 Jul 2014 13:15:50 +0200 |
blanchet |
reordered provers
|
file |
diff |
annotate
|
| Sun, 29 Jun 2014 18:28:27 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
| Tue, 24 Jun 2014 08:19:55 +0200 |
blanchet |
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
|
file |
diff |
annotate
|
| Wed, 18 Jun 2014 15:23:40 +0200 |
blanchet |
more generous formula -- there are lots of duplicates out there
|
file |
diff |
annotate
|
| Wed, 18 Jun 2014 14:19:42 +0200 |
blanchet |
automatically learn MaSh facts also in 'blocking' mode
|
file |
diff |
annotate
|
| Thu, 12 Jun 2014 17:10:12 +0200 |
blanchet |
renamed Sledgehammer options
|
file |
diff |
annotate
|
| Thu, 12 Jun 2014 17:02:03 +0200 |
blanchet |
took out broken support for Yices from SMT2 stack -- see 'NEWS' for rationale
|
file |
diff |
annotate
|
| Wed, 11 Jun 2014 11:28:46 +0200 |
blanchet |
removed '_new' sufffix in SMT2 solver names (in some cases)
|
file |
diff |
annotate
|
| Wed, 11 Jun 2014 11:28:46 +0200 |
blanchet |
removed old SMT module from Sledgehammer
|
file |
diff |
annotate
|
| Mon, 02 Jun 2014 15:10:18 +0200 |
fleury |
basic setup for zipperposition prover
|
file |
diff |
annotate
|
| Fri, 16 May 2014 19:13:50 +0200 |
blanchet |
silence methods even better
|
file |
diff |
annotate
|
| Thu, 15 May 2014 20:48:13 +0200 |
blanchet |
new approach to silence proof methods, to avoid weird theory/context mismatches
|
file |
diff |
annotate
|
| Sun, 04 May 2014 18:14:58 +0200 |
blanchet |
improved whitelist (cf. be1874de8344)
|
file |
diff |
annotate
|
| Sat, 19 Apr 2014 19:52:02 +0200 |
wenzelm |
more elementary option sledgehammer_provers, avoiding complications of defaults from ML side (NB: guessing at number of cores does not make sense in PIDE);
|
file |
diff |
annotate
|