| Fri, 02 Dec 2011 14:54:25 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
avoid that var names get changed by resolution in Metis lambda-lifting
|
file |
diff |
annotate
|
| Mon, 25 Jul 2011 14:10:12 +0200 |
blanchet |
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
|
file |
diff |
annotate
|
| Thu, 14 Jul 2011 15:14:37 +0200 |
blanchet |
always unfold "Let"s is Sledgehammer, Metis, and MESON
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
don't needlessly presimplify -- makes ATP problem preparation much faster
|
file |
diff |
annotate
|
| Tue, 17 May 2011 15:11:36 +0200 |
blanchet |
use antiquotation
|
file |
diff |
annotate
|
| Fri, 13 May 2011 22:55:00 +0200 |
wenzelm |
proper Proof.context for classical tactics;
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
another concession to backward compatibility
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
added unfold set constant functionality to Meson/Metis -- disabled by default for now
|
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
|
| Fri, 22 Apr 2011 13:58:13 +0200 |
wenzelm |
modernized Quantifier1 simproc setup;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Thu, 14 Apr 2011 11:24:05 +0200 |
blanchet |
remove experimental code added in 85bb6fbb8e6a
|
file |
diff |
annotate
|
| Thu, 14 Apr 2011 11:24:04 +0200 |
blanchet |
experiment with definitional CNF
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 22:36:24 +0100 |
blanchet |
renamed "trace_me{son,tis}" and "verbose_metis" to have the name of the tool first
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 12:49:05 +0200 |
blanchet |
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
|
file |
diff |
annotate
|
| Mon, 11 Oct 2010 18:03:18 +0700 |
blanchet |
added "trace_meson" configuration option, replacing old-fashioned reference
|
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
|
| Tue, 05 Oct 2010 10:59:12 +0200 |
blanchet |
got rid of overkill "meson_choice" attribute;
|
file |
diff |
annotate
|
| Mon, 04 Oct 2010 21:49:07 +0200 |
blanchet |
move Meson to Plain
|
file |
diff |
annotate
|
| Mon, 04 Oct 2010 21:37:42 +0200 |
blanchet |
move MESON files together
|
file |
diff |
annotate
| base
|