| Fri, 25 Oct 2024 15:31:58 +0200 |
blanchet |
variable instantiation in Sledgehammer and Metis
|
file |
diff |
annotate
|
| Thu, 28 Sep 2023 20:07:30 +0200 |
wenzelm |
explicitly reject 'handle' with catch-all patterns;
|
file |
diff |
annotate
|
| Mon, 13 Feb 2023 15:01:58 +0100 |
blanchet |
careful eta-contraction in Metis to keep argument to All and Ex expanded
|
file |
diff |
annotate
|
| Sun, 06 Jan 2019 15:04:34 +0100 |
wenzelm |
isabelle update -u path_cartouches;
|
file |
diff |
annotate
|
| Sat, 26 Mar 2016 12:22:15 +0100 |
wenzelm |
avoid hardwired values;
|
file |
diff |
annotate
|
| Fri, 18 Mar 2016 21:21:09 +0100 |
wenzelm |
clarified print depth;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Wed, 29 Oct 2014 14:05:36 +0100 |
wenzelm |
modernized setup;
|
file |
diff |
annotate
|
| Tue, 13 May 2014 11:10:23 +0200 |
blanchet |
hide more internal names
|
file |
diff |
annotate
|
| Tue, 25 Mar 2014 19:03:02 +0100 |
wenzelm |
proper configuration option "ML_print_depth";
|
file |
diff |
annotate
|
| Sun, 16 Feb 2014 13:56:48 +0100 |
haftmann |
eliminated odd dislocation of keyword declaration and implementation (leftover from 318cd8ac1817)
|
file |
diff |
annotate
|
| Thu, 30 Jan 2014 13:38:28 +0100 |
blanchet |
added 'algebra' and 'meson' to 'try0'
|
file |
diff |
annotate
|
| Fri, 18 Oct 2013 10:43:21 +0200 |
blanchet |
killed more "no_atp"s
|
file |
diff |
annotate
|
| Sat, 13 Jul 2013 00:50:49 +0200 |
wenzelm |
hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| Mon, 21 May 2012 10:39:32 +0200 |
blanchet |
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 22:08:53 +0100 |
wenzelm |
declare command keywords via theory header, including strict checking outside Pure;
|
file |
diff |
annotate
|
| Fri, 24 Feb 2012 11:23:34 +0100 |
blanchet |
renamed 'try_methods' to 'try0'
|
file |
diff |
annotate
|
| Mon, 23 Jan 2012 17:40:32 +0100 |
blanchet |
renamed two files to make room for a new file
|
file |
diff |
annotate
|
| Tue, 15 Nov 2011 22:13:39 +0100 |
blanchet |
continued implementation of lambda-lifting in Metis
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 14:43:20 +0200 |
blanchet |
renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
first step in sharing more code between ATP and Metis translation
|
file |
diff |
annotate
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
renamed "try" "try_methods"
|
file |
diff |
annotate
|
| Mon, 02 May 2011 16:33:21 +0200 |
wenzelm |
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
|
file |
diff |
annotate
|
| Thu, 14 Apr 2011 11:24:05 +0200 |
blanchet |
make 48170228f562 work also with "HO_Reas" examples
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 11:26:28 +0100 |
blanchet |
added Sledgehammer support for higher-order propositional reasoning
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 09:58:56 +0100 |
blanchet |
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
|
file |
diff |
annotate
|
| Mon, 11 Oct 2010 18:03:47 +0700 |
blanchet |
"setup" in theory
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 12:04:49 +0200 |
blanchet |
hide one more name
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 11:45:10 +0200 |
blanchet |
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
|
file |
diff |
annotate
|
| Mon, 04 Oct 2010 22:51:53 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 04 Oct 2010 22:45:09 +0200 |
blanchet |
move Metis into Plain
|
file |
diff |
annotate
|
| Wed, 20 Jun 2007 22:07:52 +0200 |
wenzelm |
The Metis prover (slightly modified version from Larry);
|
file |
diff |
annotate
|