| Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Sun, 21 Dec 2014 22:49:40 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 21 Dec 2014 15:03:45 +0100 |
wenzelm |
proper context;
|
file |
diff |
annotate
|
| Sat, 20 Dec 2014 22:23:37 +0100 |
wenzelm |
proper context for "net" tactics;
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Mon, 10 Nov 2014 21:49:48 +0100 |
wenzelm |
proper context for assume_tac (atac remains as fall-back without context);
|
file |
diff |
annotate
|
| Sun, 09 Nov 2014 17:04:14 +0100 |
wenzelm |
proper context for match_tac etc.;
|
file |
diff |
annotate
|
| Thu, 30 Oct 2014 22:45:19 +0100 |
wenzelm |
eliminated aliases;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Fri, 07 Mar 2014 22:30:58 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
| Thu, 30 May 2013 12:35:40 +0200 |
wenzelm |
standardized aliases;
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Thu, 03 Jan 2013 14:41:05 +0100 |
blanchet |
tuned comment
|
file |
diff |
annotate
|
| Thu, 03 Jan 2013 13:11:04 +0100 |
blanchet |
avoid explosion in higher-order unification algorithm
|
file |
diff |
annotate
|
| Tue, 22 May 2012 16:59:27 +0200 |
blanchet |
don't apply "ext_cong_neq" to biimplications
|
file |
diff |
annotate
|
| Tue, 22 May 2012 16:59:27 +0200 |
blanchet |
make higher-order goals more first-order via extensionality
|
file |
diff |
annotate
|
| Tue, 22 May 2012 16:59:27 +0200 |
blanchet |
added "ext_cong_neq" lemma (not used yet); tuning
|
file |
diff |
annotate
|
| Tue, 20 Mar 2012 00:44:30 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 19 Mar 2012 21:10:33 +0100 |
wenzelm |
moved some legacy stuff;
|
file |
diff |
annotate
|
| Tue, 13 Mar 2012 16:40:06 +0100 |
wenzelm |
prefer abs_def over def_raw;
|
file |
diff |
annotate
|
| Sun, 04 Mar 2012 23:20:43 +0100 |
blanchet |
ensure no abstractions leak through after lambda-lifting (for formulas with higher-order occurrences of quantifiers)
|
file |
diff |
annotate
|
| Thu, 16 Feb 2012 16:42:26 +0100 |
wenzelm |
explicit is better than implicit;
|
file |
diff |
annotate
|
| Tue, 03 Jan 2012 18:33:18 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 02 Jan 2012 14:12:20 +0100 |
blanchet |
killed unfold_set_const option that makes no sense now that set is a type constructor again
|
file |
diff |
annotate
|
| Sat, 24 Dec 2011 16:14:58 +0100 |
haftmann |
dropped references to obsolete facts `mem_def_raw` and `Collect_def_raw`
|
file |
diff |
annotate
|
| 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
|